inductive Aesop.BaseRuleSetMember : Type

• normRule (r : Aesop.NormRule) : Aesop.BaseRuleSetMember
• unsafeRule (r : Aesop.UnsafeRule) : Aesop.BaseRuleSetMember
• safeRule (r : Aesop.SafeRule) : Aesop.BaseRuleSetMember
• unfoldRule (r : Aesop.UnfoldRule) : Aesop.BaseRuleSetMember

instance Aesop.instInhabitedBaseRuleSetMember : Inhabited Aesop.BaseRuleSetMember

Equations

• Aesop.instInhabitedBaseRuleSetMember = { default := Aesop.BaseRuleSetMember.normRule default }

def Aesop.BaseRuleSetMember.name : Aesop.BaseRuleSetMember → Aesop.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

inductive Aesop.GlobalRuleSetMember : Type

• base (m : Aesop.BaseRuleSetMember) : Aesop.GlobalRuleSetMember
• normSimpRule (e : Aesop.NormSimpRule) : Aesop.GlobalRuleSetMember

instance Aesop.instInhabitedGlobalRuleSetMember : Inhabited Aesop.GlobalRuleSetMember

Equations

• Aesop.instInhabitedGlobalRuleSetMember = { default := Aesop.GlobalRuleSetMember.base default }

def Aesop.GlobalRuleSetMember.name : Aesop.GlobalRuleSetMember → Aesop.RuleName

Equations

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

inductive Aesop.LocalRuleSetMember : Type

• global (m : Aesop.GlobalRuleSetMember) : Aesop.LocalRuleSetMember
• localNormSimpRule (r : Aesop.LocalNormSimpRule) : Aesop.LocalRuleSetMember

instance Aesop.instInhabitedLocalRuleSetMember : Inhabited Aesop.LocalRuleSetMember

Equations

• Aesop.instInhabitedLocalRuleSetMember = { default := Aesop.LocalRuleSetMember.global default }

def Aesop.LocalRuleSetMember.name : Aesop.LocalRuleSetMember → Aesop.RuleName

Equations

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

def Aesop.LocalRuleSetMember.toGlobalRuleSetMember? : Aesop.LocalRuleSetMember → Option Aesop.GlobalRuleSetMember

Equations

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