inductive Aesop.BaseRuleSetMember : Type

• 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

instance Aesop.instInhabitedBaseRuleSetMember : Inhabited BaseRuleSetMember

Equations

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

def Aesop.instInhabitedBaseRuleSetMember.default : BaseRuleSetMember

Equations

• Aesop.instInhabitedBaseRuleSetMember.default = Aesop.BaseRuleSetMember.normRule 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

inductive Aesop.GlobalRuleSetMember : Type

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

instance Aesop.instInhabitedGlobalRuleSetMember : Inhabited GlobalRuleSetMember

Equations

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

def Aesop.instInhabitedGlobalRuleSetMember.default : GlobalRuleSetMember

Equations

• Aesop.instInhabitedGlobalRuleSetMember.default = Aesop.GlobalRuleSetMember.base default

def Aesop.GlobalRuleSetMember.name : GlobalRuleSetMember → RuleName

Equations

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

inductive Aesop.LocalRuleSetMember : Type

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

instance Aesop.instInhabitedLocalRuleSetMember : Inhabited LocalRuleSetMember

Equations

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

def Aesop.instInhabitedLocalRuleSetMember.default : LocalRuleSetMember

Equations

• Aesop.instInhabitedLocalRuleSetMember.default = Aesop.LocalRuleSetMember.global default

def Aesop.LocalRuleSetMember.name : LocalRuleSetMember → RuleName

Equations

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

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

Equations

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