inductive Aesop.PhaseName : Type

• norm : PhaseName
• safe : PhaseName
• unsafe : PhaseName

instance Aesop.instInhabitedPhaseName : Inhabited PhaseName

Equations

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

instance Aesop.instBEqPhaseName : BEq PhaseName

Equations

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

instance Aesop.instHashablePhaseName : Hashable PhaseName

Equations

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

instance Aesop.PhaseName.instOrd : Ord PhaseName

Equations

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

instance Aesop.PhaseName.instToString : ToString PhaseName

Equations

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

inductive Aesop.ScopeName : Type

• global : ScopeName
• local : ScopeName

instance Aesop.instInhabitedScopeName : Inhabited ScopeName

Equations

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

instance Aesop.instBEqScopeName : BEq ScopeName

Equations

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

instance Aesop.instHashableScopeName : Hashable ScopeName

Equations

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

instance Aesop.ScopeName.instOrd : Ord ScopeName

Equations

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

instance Aesop.ScopeName.instToString : ToString ScopeName

Equations

• Aesop.ScopeName.instToString = { toString := fun (x : Aesop.ScopeName) => match x with | Aesop.ScopeName.global => "global" | Aesop.ScopeName.local => "local" }

inductive Aesop.BuilderName : Type

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

instance Aesop.instInhabitedBuilderName : Inhabited BuilderName

Equations

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

instance Aesop.instBEqBuilderName : BEq BuilderName

Equations

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

instance Aesop.instHashableBuilderName : Hashable BuilderName

Equations

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

instance Aesop.BuilderName.instOrd : Ord BuilderName

Equations

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

instance Aesop.BuilderName.instToString : ToString BuilderName

Equations

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

structure Aesop.RuleName : Type

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

instance Aesop.instInhabitedRuleName : Inhabited RuleName

Equations

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

instance Aesop.RuleName.instHashable : Hashable RuleName

Equations

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

instance Aesop.RuleName.instBEq : BEq RuleName

Equations

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

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

Equations

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

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

Equations

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

instance Aesop.RuleName.instOrd : Ord RuleName

Equations

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

instance Aesop.RuleName.instToString : ToString RuleName

Equations

• Aesop.RuleName.instToString = { toString := fun (n : Aesop.RuleName) => toString n.phase ++ "|" ++ toString n.builder ++ "|" ++ toString n.scope ++ "|" ++ toString n.name }

def Aesop.getRuleNameForExpr : Lean.Expr → Lean.MetaM Lean.Name

Equations

• Aesop.getRuleNameForExpr (Lean.Expr.const decl us) = pure decl
• Aesop.getRuleNameForExpr (Lean.Expr.fvar fvarId) = do let __do_lift ← fvarId.getDecl pure __do_lift.userName
• Aesop.getRuleNameForExpr x✝ = Lean.mkFreshId

inductive Aesop.DisplayRuleName : Type

• ruleName (n : RuleName) : DisplayRuleName
• normSimp : DisplayRuleName
• normUnfold : DisplayRuleName

instance Aesop.instInhabitedDisplayRuleName : Inhabited DisplayRuleName

Equations

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

instance Aesop.instBEqDisplayRuleName : BEq DisplayRuleName

Equations

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

instance Aesop.instOrdDisplayRuleName : Ord DisplayRuleName

Equations

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

instance Aesop.instHashableDisplayRuleName : Hashable DisplayRuleName

Equations

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

instance Aesop.DisplayRuleName.instCoeRuleName : Coe RuleName DisplayRuleName

Equations

• Aesop.DisplayRuleName.instCoeRuleName = { coe := Aesop.DisplayRuleName.ruleName }

instance Aesop.DisplayRuleName.instToString : ToString DisplayRuleName

Equations

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