inductive Aesop.PhaseName : Type

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

@[implicit_reducible]

instance Aesop.instInhabitedPhaseName : Inhabited PhaseName

Equations

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

def Aesop.instInhabitedPhaseName.default : PhaseName

Equations

• Aesop.instInhabitedPhaseName.default = Aesop.PhaseName.norm

def Aesop.instBEqPhaseName.beq : PhaseName → PhaseName → Bool

Equations

• Aesop.instBEqPhaseName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Aesop.instBEqPhaseName : BEq PhaseName

Equations

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

@[implicit_reducible]

instance Aesop.instHashablePhaseName : Hashable PhaseName

Equations

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

def Aesop.instHashablePhaseName.hash : PhaseName → UInt64

Equations

• Aesop.instHashablePhaseName.hash Aesop.PhaseName.norm = 0
• Aesop.instHashablePhaseName.hash Aesop.PhaseName.safe = 1
• Aesop.instHashablePhaseName.hash Aesop.PhaseName.unsafe = 2

@[implicit_reducible]

instance Aesop.instToJsonPhaseName : Lean.ToJson PhaseName

Equations

• Aesop.instToJsonPhaseName = { toJson := Aesop.instToJsonPhaseName.toJson }

def Aesop.instToJsonPhaseName.toJson : PhaseName → Lean.Json

Equations

• Aesop.instToJsonPhaseName.toJson Aesop.PhaseName.norm = Lean.toJson "norm"
• Aesop.instToJsonPhaseName.toJson Aesop.PhaseName.safe = Lean.toJson "safe"
• Aesop.instToJsonPhaseName.toJson Aesop.PhaseName.unsafe = Lean.toJson "unsafe"

@[implicit_reducible]

instance Aesop.PhaseName.instOrd : Ord PhaseName

Equations

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

@[implicit_reducible]

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

def Aesop.instInhabitedScopeName.default : ScopeName

Equations

• Aesop.instInhabitedScopeName.default = Aesop.ScopeName.global

@[implicit_reducible]

instance Aesop.instInhabitedScopeName : Inhabited ScopeName

Equations

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

def Aesop.instBEqScopeName.beq : ScopeName → ScopeName → Bool

Equations

• Aesop.instBEqScopeName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Aesop.instBEqScopeName : BEq ScopeName

Equations

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

@[implicit_reducible]

instance Aesop.instHashableScopeName : Hashable ScopeName

Equations

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

def Aesop.instHashableScopeName.hash : ScopeName → UInt64

Equations

• Aesop.instHashableScopeName.hash Aesop.ScopeName.global = 0
• Aesop.instHashableScopeName.hash Aesop.ScopeName.local = 1

def Aesop.instToJsonScopeName.toJson : ScopeName → Lean.Json

Equations

• Aesop.instToJsonScopeName.toJson Aesop.ScopeName.global = Lean.toJson "global"
• Aesop.instToJsonScopeName.toJson Aesop.ScopeName.local = Lean.toJson "local"

@[implicit_reducible]

instance Aesop.instToJsonScopeName : Lean.ToJson ScopeName

Equations

• Aesop.instToJsonScopeName = { toJson := Aesop.instToJsonScopeName.toJson }

@[implicit_reducible]

instance Aesop.ScopeName.instOrd : Ord ScopeName

Equations

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

@[implicit_reducible]

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

def Aesop.instInhabitedBuilderName.default : BuilderName

Equations

• Aesop.instInhabitedBuilderName.default = Aesop.BuilderName.apply

@[implicit_reducible]

instance Aesop.instInhabitedBuilderName : Inhabited BuilderName

Equations

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

def Aesop.instBEqBuilderName.beq : BuilderName → BuilderName → Bool

Equations

• Aesop.instBEqBuilderName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Aesop.instBEqBuilderName : BEq BuilderName

Equations

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

@[implicit_reducible]

instance Aesop.instHashableBuilderName : Hashable BuilderName

Equations

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

def Aesop.instHashableBuilderName.hash : BuilderName → UInt64

Equations

• Aesop.instHashableBuilderName.hash Aesop.BuilderName.apply = 0
• Aesop.instHashableBuilderName.hash Aesop.BuilderName.cases = 1
• Aesop.instHashableBuilderName.hash Aesop.BuilderName.constructors = 2
• Aesop.instHashableBuilderName.hash Aesop.BuilderName.destruct = 3
• Aesop.instHashableBuilderName.hash Aesop.BuilderName.forward = 4
• Aesop.instHashableBuilderName.hash Aesop.BuilderName.simp = 5
• Aesop.instHashableBuilderName.hash Aesop.BuilderName.tactic = 6
• Aesop.instHashableBuilderName.hash Aesop.BuilderName.unfold = 7

def Aesop.instToJsonBuilderName.toJson : BuilderName → Lean.Json

Equations

• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.apply = Lean.toJson "apply"
• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.cases = Lean.toJson "cases"
• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.constructors = Lean.toJson "constructors"
• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.destruct = Lean.toJson "destruct"
• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.forward = Lean.toJson "forward"
• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.simp = Lean.toJson "simp"
• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.tactic = Lean.toJson "tactic"
• Aesop.instToJsonBuilderName.toJson Aesop.BuilderName.unfold = Lean.toJson "unfold"

@[implicit_reducible]

instance Aesop.instToJsonBuilderName : Lean.ToJson BuilderName

Equations

• Aesop.instToJsonBuilderName = { toJson := Aesop.instToJsonBuilderName.toJson }

@[implicit_reducible]

instance Aesop.BuilderName.instOrd : Ord BuilderName

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Aesop.instInhabitedRuleName : Inhabited RuleName

Equations

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

def Aesop.instInhabitedRuleName.default : RuleName

Equations

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

@[implicit_reducible]

instance Aesop.RuleName.instHashable : Hashable RuleName

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Aesop.RuleName.instOrd : Ord RuleName

Equations

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

@[implicit_reducible]

instance Aesop.RuleName.instToString : ToString RuleName

Equations

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

@[implicit_reducible]

instance Aesop.RuleName.instToJson : Lean.ToJson RuleName

Equations

• Aesop.RuleName.instToJson = { toJson := fun (n : Aesop.RuleName) => Aesop.RuleName.instToJson._private_1 n }

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

def Aesop.instInhabitedDisplayRuleName.default : DisplayRuleName

Equations

• Aesop.instInhabitedDisplayRuleName.default = Aesop.DisplayRuleName.ruleName default

@[implicit_reducible]

instance Aesop.instInhabitedDisplayRuleName : Inhabited DisplayRuleName

Equations

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

@[implicit_reducible]

instance Aesop.instBEqDisplayRuleName : BEq DisplayRuleName

Equations

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

def Aesop.instBEqDisplayRuleName.beq : DisplayRuleName → DisplayRuleName → Bool

Equations

• Aesop.instBEqDisplayRuleName.beq (Aesop.DisplayRuleName.ruleName a) (Aesop.DisplayRuleName.ruleName b) = (a == b)
• Aesop.instBEqDisplayRuleName.beq Aesop.DisplayRuleName.normSimp Aesop.DisplayRuleName.normSimp = true
• Aesop.instBEqDisplayRuleName.beq Aesop.DisplayRuleName.normUnfold Aesop.DisplayRuleName.normUnfold = true
• Aesop.instBEqDisplayRuleName.beq x✝¹ x✝ = false

def Aesop.instOrdDisplayRuleName.ord : DisplayRuleName → DisplayRuleName → Ordering

Equations

• Aesop.instOrdDisplayRuleName.ord (Aesop.DisplayRuleName.ruleName a) (Aesop.DisplayRuleName.ruleName b) = (compare a b).then Ordering.eq
• Aesop.instOrdDisplayRuleName.ord (Aesop.DisplayRuleName.ruleName a) x✝ = Ordering.lt
• Aesop.instOrdDisplayRuleName.ord x✝ (Aesop.DisplayRuleName.ruleName a) = Ordering.gt
• Aesop.instOrdDisplayRuleName.ord Aesop.DisplayRuleName.normSimp Aesop.DisplayRuleName.normSimp = Ordering.eq
• Aesop.instOrdDisplayRuleName.ord Aesop.DisplayRuleName.normSimp x✝ = Ordering.lt
• Aesop.instOrdDisplayRuleName.ord x✝ Aesop.DisplayRuleName.normSimp = Ordering.gt
• Aesop.instOrdDisplayRuleName.ord Aesop.DisplayRuleName.normUnfold Aesop.DisplayRuleName.normUnfold = Ordering.eq

@[implicit_reducible]

instance Aesop.instOrdDisplayRuleName : Ord DisplayRuleName

Equations

• Aesop.instOrdDisplayRuleName = { compare := Aesop.instOrdDisplayRuleName.ord }

@[implicit_reducible]

instance Aesop.instHashableDisplayRuleName : Hashable DisplayRuleName

Equations

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

def Aesop.instHashableDisplayRuleName.hash : DisplayRuleName → UInt64

Equations

• Aesop.instHashableDisplayRuleName.hash (Aesop.DisplayRuleName.ruleName a) = mixHash 0 (hash a)
• Aesop.instHashableDisplayRuleName.hash Aesop.DisplayRuleName.normSimp = 1
• Aesop.instHashableDisplayRuleName.hash Aesop.DisplayRuleName.normUnfold = 2

@[implicit_reducible]

instance Aesop.DisplayRuleName.instCoeRuleName : Coe RuleName DisplayRuleName

Equations

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

@[implicit_reducible]

instance Aesop.DisplayRuleName.instToString : ToString DisplayRuleName

Equations

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

@[implicit_reducible]

instance Aesop.DisplayRuleName.instToJson : Lean.ToJson DisplayRuleName

Equations

• Aesop.DisplayRuleName.instToJson = { toJson := fun (n : Aesop.DisplayRuleName) => Aesop.DisplayRuleName.instToJson._private_1 n }