inductive Aesop.PhaseName : Type

• norm: Aesop.PhaseName
• safe: Aesop.PhaseName
• unsafe: Aesop.PhaseName

instance Aesop.instInhabitedPhaseName : Inhabited Aesop.PhaseName

Equations

• Aesop.instInhabitedPhaseName = { default := Aesop.PhaseName.norm }

instance Aesop.instBEqPhaseName : BEq Aesop.PhaseName

Equations

• Aesop.instBEqPhaseName = { beq := Aesop.beqPhaseName✝ }

instance Aesop.instHashablePhaseName : Hashable Aesop.PhaseName

Equations

• Aesop.instHashablePhaseName = { hash := Aesop.hashPhaseName✝ }

instance Aesop.PhaseName.instOrdPhaseName : Ord Aesop.PhaseName

Equations

• Aesop.PhaseName.instOrdPhaseName = { compare := fun (s₁ s₂ : Aesop.PhaseName) => compare (Aesop.PhaseName.toCtorIdx s₁) (Aesop.PhaseName.toCtorIdx s₂) }

instance Aesop.PhaseName.instToStringPhaseName : ToString Aesop.PhaseName

Equations

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

inductive Aesop.ScopeName : Type

• global: Aesop.ScopeName
• local: Aesop.ScopeName

instance Aesop.instInhabitedScopeName : Inhabited Aesop.ScopeName

Equations

• Aesop.instInhabitedScopeName = { default := Aesop.ScopeName.global }

instance Aesop.instBEqScopeName : BEq Aesop.ScopeName

Equations

• Aesop.instBEqScopeName = { beq := Aesop.beqScopeName✝ }

instance Aesop.instHashableScopeName : Hashable Aesop.ScopeName

Equations

• Aesop.instHashableScopeName = { hash := Aesop.hashScopeName✝ }

instance Aesop.ScopeName.instOrdScopeName : Ord Aesop.ScopeName

Equations

• Aesop.ScopeName.instOrdScopeName = { compare := fun (s₁ s₂ : Aesop.ScopeName) => compare (Aesop.ScopeName.toCtorIdx s₁) (Aesop.ScopeName.toCtorIdx s₂) }

instance Aesop.ScopeName.instToStringScopeName : ToString Aesop.ScopeName

Equations

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

inductive Aesop.BuilderName : Type

• apply: Aesop.BuilderName
• cases: Aesop.BuilderName
• constructors: Aesop.BuilderName
• destruct: Aesop.BuilderName
• forward: Aesop.BuilderName
• simp: Aesop.BuilderName
• tactic: Aesop.BuilderName
• unfold: Aesop.BuilderName

instance Aesop.instInhabitedBuilderName : Inhabited Aesop.BuilderName

Equations

• Aesop.instInhabitedBuilderName = { default := Aesop.BuilderName.apply }

instance Aesop.instBEqBuilderName : BEq Aesop.BuilderName

Equations

• Aesop.instBEqBuilderName = { beq := Aesop.beqBuilderName✝ }

instance Aesop.instHashableBuilderName : Hashable Aesop.BuilderName

Equations

• Aesop.instHashableBuilderName = { hash := Aesop.hashBuilderName✝ }

instance Aesop.BuilderName.instOrdBuilderName : Ord Aesop.BuilderName

Equations

• Aesop.BuilderName.instOrdBuilderName = { compare := fun (b₁ b₂ : Aesop.BuilderName) => compare (Aesop.BuilderName.toCtorIdx b₁) (Aesop.BuilderName.toCtorIdx b₂) }

instance Aesop.BuilderName.instToStringBuilderName : ToString Aesop.BuilderName

Equations

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

structure Aesop.RuleName : Type

• name : Lean.Name
• builder : Aesop.BuilderName
• phase : Aesop.PhaseName
• scope : Aesop.ScopeName
• hash : UInt64

instance Aesop.instInhabitedRuleName : Inhabited Aesop.RuleName

Equations

• Aesop.instInhabitedRuleName = { default := { name := default, builder := default, phase := default, scope := default, hash := default } }

instance Aesop.RuleName.instHashableRuleName : Hashable Aesop.RuleName

Equations

• Aesop.RuleName.instHashableRuleName = { hash := fun (n : Aesop.RuleName) => n.hash }

instance Aesop.RuleName.instBEqRuleName : BEq Aesop.RuleName

Equations

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

def Aesop.RuleName.compare : Aesop.RuleName → Aesop.RuleName → Ordering

Equations

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

def Aesop.RuleName.quickCompare (n₁ : Aesop.RuleName) (n₂ : Aesop.RuleName) : Ordering

Equations

• Aesop.RuleName.quickCompare n₁ n₂ = match compare n₁.hash n₂.hash with | Ordering.eq => Aesop.RuleName.compare n₁ n₂ | ord => ord

instance Aesop.RuleName.instOrdRuleName : Ord Aesop.RuleName

Equations

• Aesop.RuleName.instOrdRuleName = { compare := Aesop.RuleName.compare }

instance Aesop.RuleName.instToStringRuleName : ToString Aesop.RuleName

Equations

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

inductive Aesop.DisplayRuleName : Type

• ruleName: Aesop.RuleName → Aesop.DisplayRuleName
• normSimp: Aesop.DisplayRuleName
• normUnfold: Aesop.DisplayRuleName

instance Aesop.instInhabitedDisplayRuleName : Inhabited Aesop.DisplayRuleName

Equations

• Aesop.instInhabitedDisplayRuleName = { default := Aesop.DisplayRuleName.ruleName default }

instance Aesop.instBEqDisplayRuleName : BEq Aesop.DisplayRuleName

Equations

• Aesop.instBEqDisplayRuleName = { beq := Aesop.beqDisplayRuleName✝ }

instance Aesop.instOrdDisplayRuleName : Ord Aesop.DisplayRuleName

Equations

• Aesop.instOrdDisplayRuleName = { compare := Aesop.ordDisplayRuleName✝ }

instance Aesop.instHashableDisplayRuleName : Hashable Aesop.DisplayRuleName

Equations

• Aesop.instHashableDisplayRuleName = { hash := Aesop.hashDisplayRuleName✝ }

instance Aesop.DisplayRuleName.instToStringDisplayRuleName : ToString Aesop.DisplayRuleName

Equations

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

inductive Aesop.RuleIdent : Type

• const: Lean.Name → Aesop.RuleIdent
• fvar: Lean.Name → Aesop.RuleIdent

instance Aesop.instInhabitedRuleIdent : Inhabited Aesop.RuleIdent

Equations

• Aesop.instInhabitedRuleIdent = { default := Aesop.RuleIdent.const default }

instance Aesop.instBEqRuleIdent : BEq Aesop.RuleIdent

Equations

• Aesop.instBEqRuleIdent = { beq := Aesop.beqRuleIdent✝ }

instance Aesop.instHashableRuleIdent : Hashable Aesop.RuleIdent

Equations

• Aesop.instHashableRuleIdent = { hash := Aesop.hashRuleIdent✝ }

instance Aesop.RuleIdent.instToStringRuleIdent : ToString Aesop.RuleIdent

Equations

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

def Aesop.RuleIdent.name : Aesop.RuleIdent → Lean.Name

Equations

• Aesop.RuleIdent.name x = match x with | Aesop.RuleIdent.const decl => decl | Aesop.RuleIdent.fvar userName => userName

def Aesop.RuleIdent.scope : Aesop.RuleIdent → Aesop.ScopeName

Equations

• Aesop.RuleIdent.scope x = match x with | Aesop.RuleIdent.const decl => Aesop.ScopeName.global | Aesop.RuleIdent.fvar userName => Aesop.ScopeName.local

def Aesop.RuleIdent.type : Aesop.RuleIdent → Lean.MetaM Lean.Expr

Equations

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

def Aesop.RuleIdent.toRuleName (phase : Aesop.PhaseName) (builder : Aesop.BuilderName) (i : Aesop.RuleIdent) : Aesop.RuleName

Equations

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

def Aesop.RuleName.toRuleIdent (i : Aesop.RuleName) : Aesop.RuleIdent

Equations

• Aesop.RuleName.toRuleIdent i = match i.scope with | Aesop.ScopeName.global => Aesop.RuleIdent.const i.name | Aesop.ScopeName.local => Aesop.RuleIdent.fvar i.name