Documentation

Aesop.RuleSet.Member

← Mathematical handbook

inductive Aesop.BaseRuleSetMember :

normRule (r : NormRule) : BaseRuleSetMember
unsafeRule (r : UnsafeRule) : BaseRuleSetMember
safeRule (r : SafeRule) : BaseRuleSetMember
unfoldRule (r : UnfoldRule) : BaseRuleSetMember
normForwardRule (r₁ : ForwardRule) (r₂ : NormRule) : BaseRuleSetMember
unsafeForwardRule (r₁ : ForwardRule) (r₂ : UnsafeRule) : BaseRuleSetMember
safeForwardRule (r₁ : ForwardRule) (r₂ : SafeRule) : BaseRuleSetMember

Instances For

@[instance_reducible]

instance Aesop.instInhabitedBaseRuleSetMember :

Inhabited BaseRuleSetMember

Equations

Aesop.instInhabitedBaseRuleSetMember = { default := Aesop.instInhabitedBaseRuleSetMember.default }

def Aesop.BaseRuleSetMember.name :

BaseRuleSetMember → RuleName

Equations

(Aesop.BaseRuleSetMember.normRule r).name = r.name
(Aesop.BaseRuleSetMember.unsafeRule r).name = r.name
(Aesop.BaseRuleSetMember.safeRule r).name = r.name
(Aesop.BaseRuleSetMember.unfoldRule r).name = r.name
(Aesop.BaseRuleSetMember.normForwardRule r r₂).name = r.name
(Aesop.BaseRuleSetMember.unsafeForwardRule r r₂).name = r.name
(Aesop.BaseRuleSetMember.safeForwardRule r r₂).name = r.name

Instances For

inductive Aesop.GlobalRuleSetMember :

base (m : BaseRuleSetMember) : GlobalRuleSetMember
normSimpRule (e : NormSimpRule) : GlobalRuleSetMember

Instances For

@[instance_reducible]

instance Aesop.instInhabitedGlobalRuleSetMember :

Inhabited GlobalRuleSetMember

Equations

Aesop.instInhabitedGlobalRuleSetMember = { default := Aesop.instInhabitedGlobalRuleSetMember.default }

def Aesop.GlobalRuleSetMember.name :

GlobalRuleSetMember → RuleName

Equations

(Aesop.GlobalRuleSetMember.base m).name = m.name
(Aesop.GlobalRuleSetMember.normSimpRule r).name = r.name

Instances For

inductive Aesop.LocalRuleSetMember :

global (m : GlobalRuleSetMember) : LocalRuleSetMember
localNormSimpRule (r : LocalNormSimpRule) : LocalRuleSetMember

Instances For

@[instance_reducible]

instance Aesop.instInhabitedLocalRuleSetMember :

Inhabited LocalRuleSetMember

Equations

Aesop.instInhabitedLocalRuleSetMember = { default := Aesop.instInhabitedLocalRuleSetMember.default }

def Aesop.LocalRuleSetMember.name :

LocalRuleSetMember → RuleName

Equations

(Aesop.LocalRuleSetMember.global m).name = m.name
(Aesop.LocalRuleSetMember.localNormSimpRule r).name = r.name

Instances For

def Aesop.LocalRuleSetMember.toGlobalRuleSetMember? :

LocalRuleSetMember → Option GlobalRuleSetMember

Equations

(Aesop.LocalRuleSetMember.global m).toGlobalRuleSetMember? = some m
x✝.toGlobalRuleSetMember? = none

Instances For