HepLean Documentation

Aesop.Rule.Name

inductive Aesop.PhaseName :

Instances For

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.instOrd :

Ord Aesop.PhaseName

Equations

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

instance Aesop.PhaseName.instToString :

ToString Aesop.PhaseName

Equations

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

inductive Aesop.ScopeName :

global: Aesop.ScopeName
local: Aesop.ScopeName

Instances For

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.instOrd :

Ord Aesop.ScopeName

Equations

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

instance Aesop.ScopeName.instToString :

ToString Aesop.ScopeName

Equations

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

inductive Aesop.BuilderName :

Instances For

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.instOrd :

Ord Aesop.BuilderName

Equations

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

instance Aesop.BuilderName.instToString :

ToString Aesop.BuilderName

Equations

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

structure Aesop.RuleName :

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

Instances For

instance Aesop.instInhabitedRuleName :

Inhabited Aesop.RuleName

Equations

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

instance Aesop.RuleName.instHashable :

Hashable Aesop.RuleName

Equations

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

instance Aesop.RuleName.instBEq :

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.

Instances For

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

Equations

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

Instances For

instance Aesop.RuleName.instOrd :

Ord Aesop.RuleName

Equations

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

instance Aesop.RuleName.instToString :

ToString Aesop.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

Instances For

inductive Aesop.DisplayRuleName :

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

Instances For

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.instCoeRuleName :

Coe Aesop.RuleName Aesop.DisplayRuleName

Equations

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

instance Aesop.DisplayRuleName.instToString :

ToString Aesop.DisplayRuleName

Equations

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