inductive Aesop.BaseRuleSetMember : Type

• normRule: Aesop.NormRule → Aesop.BaseRuleSetMember
• unsafeRule: Aesop.UnsafeRule → Aesop.BaseRuleSetMember
• safeRule: Aesop.SafeRule → Aesop.BaseRuleSetMember
• unfoldRule: 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

• One or more equations did not get rendered due to their size.

inductive Aesop.GlobalRuleSetMember : Type

• base: Aesop.BaseRuleSetMember → Aesop.GlobalRuleSetMember
• normSimpRule: 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

• x.name = match x with | Aesop.GlobalRuleSetMember.base m => m.name | Aesop.GlobalRuleSetMember.normSimpRule r => r.name

inductive Aesop.LocalRuleSetMember : Type

• global: Aesop.GlobalRuleSetMember → Aesop.LocalRuleSetMember
• localNormSimpRule: 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

• x.name = match x with | Aesop.LocalRuleSetMember.global m => m.name | Aesop.LocalRuleSetMember.localNormSimpRule r => r.name

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

Equations

• x.toGlobalRuleSetMember? = match x with | Aesop.LocalRuleSetMember.global m => some m | x => none