Instances For
Equations
Equations
- Aesop.instBEqPhaseName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
Equations
Equations
- Aesop.PhaseName.instOrd = { compare := fun (s₁ s₂ : Aesop.PhaseName) => compare s₁.ctorIdx s₂.ctorIdx }
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
- Aesop.instBEqScopeName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
Equations
Equations
- Aesop.ScopeName.instOrd = { compare := fun (s₁ s₂ : Aesop.ScopeName) => compare s₁.ctorIdx s₂.ctorIdx }
Equations
- Aesop.ScopeName.instToString = { toString := fun (x : Aesop.ScopeName) => match x with | Aesop.ScopeName.global => "global" | Aesop.ScopeName.local => "local" }
- apply : BuilderName
- cases : BuilderName
- constructors : BuilderName
- destruct : BuilderName
- forward : BuilderName
- simp : BuilderName
- tactic : BuilderName
- unfold : BuilderName
Instances For
Equations
Instances For
Equations
- Aesop.instBEqBuilderName.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Equations
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
Instances For
Equations
Equations
- Aesop.BuilderName.instOrd = { compare := fun (b₁ b₂ : Aesop.BuilderName) => compare b₁.ctorIdx b₂.ctorIdx }
Equations
- One or more equations did not get rendered due to their size.
- name : Lean.Name
- builder : BuilderName
- phase : PhaseName
- scope : ScopeName
- hash : UInt64
Instances For
Equations
Equations
- Aesop.RuleName.instHashable = { hash := fun (n : Aesop.RuleName) => n.hash }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- n₁.quickCompare n₂ = match compare n₁.hash n₂.hash with | Ordering.eq => n₁.compare n₂ | ord => ord
Instances For
Equations
- Aesop.RuleName.instOrd = { compare := Aesop.RuleName.compare }
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
Instances For
- ruleName (n : RuleName) : DisplayRuleName
- normSimp : DisplayRuleName
- normUnfold : DisplayRuleName
Instances For
Equations
Equations
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
Instances For
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 b) = 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
Instances For
Equations
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.