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

Ord Aesop.PhaseName

Equations

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

instance Aesop.PhaseName.instToStringPhaseName :

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

Ord Aesop.ScopeName

Equations

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

instance Aesop.ScopeName.instToStringScopeName :

ToString Aesop.ScopeName

Equations

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

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

Ord Aesop.BuilderName

Equations

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

instance Aesop.BuilderName.instToStringBuilderName :

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

Hashable Aesop.RuleName

Equations

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

instance Aesop.RuleName.instBEqRuleName :

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

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

Instances For

instance Aesop.RuleName.instOrdRuleName :

Ord Aesop.RuleName

Equations

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

instance Aesop.RuleName.instToStringRuleName :

ToString Aesop.RuleName

Equations

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

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

ToString Aesop.DisplayRuleName

Equations

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