- norm: Aesop.PhaseName
- safe: Aesop.PhaseName
- unsafe: Aesop.PhaseName
Instances For
Equations
- Aesop.instInhabitedPhaseName = { default := Aesop.PhaseName.norm }
Equations
- Aesop.instBEqPhaseName = { beq := Aesop.beqPhaseName✝ }
Equations
- Aesop.instHashablePhaseName = { hash := Aesop.hashPhaseName✝ }
Equations
- Aesop.PhaseName.instOrd = { compare := fun (s₁ s₂ : Aesop.PhaseName) => compare s₁.toCtorIdx s₂.toCtorIdx }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Aesop.instInhabitedScopeName = { default := Aesop.ScopeName.global }
Equations
- Aesop.instBEqScopeName = { beq := Aesop.beqScopeName✝ }
Equations
- Aesop.instHashableScopeName = { hash := Aesop.hashScopeName✝ }
Equations
- Aesop.ScopeName.instOrd = { compare := fun (s₁ s₂ : Aesop.ScopeName) => compare s₁.toCtorIdx s₂.toCtorIdx }
Equations
- Aesop.ScopeName.instToString = { toString := fun (x : Aesop.ScopeName) => match x with | Aesop.ScopeName.global => "global" | Aesop.ScopeName.local => "local" }
- apply: Aesop.BuilderName
- cases: Aesop.BuilderName
- constructors: Aesop.BuilderName
- destruct: Aesop.BuilderName
- forward: Aesop.BuilderName
- simp: Aesop.BuilderName
- tactic: Aesop.BuilderName
- unfold: Aesop.BuilderName
Instances For
Equations
- Aesop.instInhabitedBuilderName = { default := Aesop.BuilderName.apply }
Equations
- Aesop.instBEqBuilderName = { beq := Aesop.beqBuilderName✝ }
Equations
- Aesop.instHashableBuilderName = { hash := Aesop.hashBuilderName✝ }
Equations
- Aesop.BuilderName.instOrd = { compare := fun (b₁ b₂ : Aesop.BuilderName) => compare b₁.toCtorIdx b₂.toCtorIdx }
Equations
- One or more equations did not get rendered due to their size.
- name : Lean.Name
- builder : Aesop.BuilderName
- phase : Aesop.PhaseName
- scope : Aesop.ScopeName
- hash : UInt64
Instances For
Equations
- Aesop.instInhabitedRuleName = { default := { name := default, builder := default, phase := default, scope := default, hash := default } }
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: Aesop.RuleName → Aesop.DisplayRuleName
- normSimp: Aesop.DisplayRuleName
- normUnfold: Aesop.DisplayRuleName
Instances For
Equations
- Aesop.instInhabitedDisplayRuleName = { default := Aesop.DisplayRuleName.ruleName default }
Equations
Equations
- Aesop.instOrdDisplayRuleName = { compare := Aesop.ordDisplayRuleName✝ }
Equations
Equations
- One or more equations did not get rendered due to their size.