Aesop.Rule.Name

source

inductive Aesop.PhaseName :

Type

Instances For

source

instance Aesop.instInhabitedPhaseName :

Inhabited Aesop.PhaseName

Equations

Aesop.instInhabitedPhaseName = { default := Aesop.PhaseName.norm }

source

instance Aesop.instBEqPhaseName :

BEq Aesop.PhaseName

Equations

Aesop.instBEqPhaseName = { beq := Aesop.beqPhaseName✝ }

source

instance Aesop.instHashablePhaseName :

Hashable Aesop.PhaseName

Equations

Aesop.instHashablePhaseName = { hash := Aesop.hashPhaseName✝ }

source

instance Aesop.PhaseName.instOrdPhaseName :

Ord Aesop.PhaseName

Equations

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

source

instance Aesop.PhaseName.instToStringPhaseName :

ToString Aesop.PhaseName

Equations

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

source

inductive Aesop.ScopeName :

Type

global: Aesop.ScopeName
local: Aesop.ScopeName

Instances For

source

instance Aesop.instInhabitedScopeName :

Inhabited Aesop.ScopeName

Equations

Aesop.instInhabitedScopeName = { default := Aesop.ScopeName.global }

source

instance Aesop.instBEqScopeName :

BEq Aesop.ScopeName

Equations

Aesop.instBEqScopeName = { beq := Aesop.beqScopeName✝ }

source

instance Aesop.instHashableScopeName :

Hashable Aesop.ScopeName

Equations

Aesop.instHashableScopeName = { hash := Aesop.hashScopeName✝ }

source

instance Aesop.ScopeName.instOrdScopeName :

Ord Aesop.ScopeName

Equations

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

source

instance Aesop.ScopeName.instToStringScopeName :

ToString Aesop.ScopeName

Equations

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

source

inductive Aesop.BuilderName :

Type

Instances For

source

instance Aesop.instInhabitedBuilderName :

Inhabited Aesop.BuilderName

Equations

Aesop.instInhabitedBuilderName = { default := Aesop.BuilderName.apply }

source

instance Aesop.instBEqBuilderName :

BEq Aesop.BuilderName

Equations

Aesop.instBEqBuilderName = { beq := Aesop.beqBuilderName✝ }

source

instance Aesop.instHashableBuilderName :

Hashable Aesop.BuilderName

Equations

Aesop.instHashableBuilderName = { hash := Aesop.hashBuilderName✝ }

source

instance Aesop.BuilderName.instOrdBuilderName :

Ord Aesop.BuilderName

Equations

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

source

instance Aesop.BuilderName.instToStringBuilderName :

ToString Aesop.BuilderName

Equations

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

source

structure Aesop.RuleName :

Type

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

Instances For

source

instance Aesop.instInhabitedRuleName :

Inhabited Aesop.RuleName

Equations

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

source

instance Aesop.RuleName.instHashableRuleName :

Hashable Aesop.RuleName

Equations

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

source

instance Aesop.RuleName.instBEqRuleName :

BEq Aesop.RuleName

Equations

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

source

def Aesop.RuleName.compare :

Aesop.RuleName → Aesop.RuleName → Ordering

Equations

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

Instances For

source

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

Ordering

Equations

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

Instances For

source

instance Aesop.RuleName.instOrdRuleName :

Ord Aesop.RuleName

Equations

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

source

instance Aesop.RuleName.instToStringRuleName :

ToString Aesop.RuleName

Equations

Aesop.RuleName.instToStringRuleName = { toString := fun n => toString n.phase ++ "|" ++ toString n.builder ++ "|" ++ toString n.scope ++ "|" ++ toString n.name }

source

inductive Aesop.DisplayRuleName :

Type

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

Instances For

source

instance Aesop.instInhabitedDisplayRuleName :

Inhabited Aesop.DisplayRuleName

Equations

Aesop.instInhabitedDisplayRuleName = { default := Aesop.DisplayRuleName.ruleName default }

source

instance Aesop.instBEqDisplayRuleName :

BEq Aesop.DisplayRuleName

Equations

Aesop.instBEqDisplayRuleName = { beq := Aesop.beqDisplayRuleName✝ }

source

instance Aesop.instOrdDisplayRuleName :

Ord Aesop.DisplayRuleName

Equations

Aesop.instOrdDisplayRuleName = { compare := Aesop.ordDisplayRuleName✝ }

source

instance Aesop.instHashableDisplayRuleName :

Hashable Aesop.DisplayRuleName

Equations

Aesop.instHashableDisplayRuleName = { hash := Aesop.hashDisplayRuleName✝ }

source

instance Aesop.DisplayRuleName.instToStringDisplayRuleName :

ToString Aesop.DisplayRuleName

Equations

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

source

inductive Aesop.RuleIdent :

Type

const: Lean.Name → Aesop.RuleIdent
fvar: Lean.Name → Aesop.RuleIdent

Instances For

source

instance Aesop.instInhabitedRuleIdent :

Inhabited Aesop.RuleIdent

Equations

Aesop.instInhabitedRuleIdent = { default := Aesop.RuleIdent.const default }

source

instance Aesop.instBEqRuleIdent :

BEq Aesop.RuleIdent

Equations

Aesop.instBEqRuleIdent = { beq := Aesop.beqRuleIdent✝ }

source

instance Aesop.instHashableRuleIdent :

Hashable Aesop.RuleIdent

Equations

Aesop.instHashableRuleIdent = { hash := Aesop.hashRuleIdent✝ }

source

instance Aesop.RuleIdent.instToStringRuleIdent :

ToString Aesop.RuleIdent

Equations

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

source

def Aesop.RuleIdent.name :

Aesop.RuleIdent → Lean.Name

Equations

Aesop.RuleIdent.name x = match x with | Aesop.RuleIdent.const decl => decl | Aesop.RuleIdent.fvar userName => userName

Instances For

source

def Aesop.RuleIdent.scope :

Aesop.RuleIdent → Aesop.ScopeName

Equations

Aesop.RuleIdent.scope x = match x with | Aesop.RuleIdent.const decl => Aesop.ScopeName.global | Aesop.RuleIdent.fvar userName => Aesop.ScopeName.local

Instances For

source

def Aesop.RuleIdent.type :

Aesop.RuleIdent → Lean.MetaM Lean.Expr

Equations

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

Instances For

source

def Aesop.RuleIdent.toRuleName (phase : Aesop.PhaseName) (builder : Aesop.BuilderName) (i : Aesop.RuleIdent) :

Aesop.RuleName

Equations

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

Instances For

source

def Aesop.RuleName.toRuleIdent (i : Aesop.RuleName) :

Aesop.RuleIdent

Equations

Aesop.RuleName.toRuleIdent i = match i.scope with | Aesop.ScopeName.global => Aesop.RuleIdent.const i.name | Aesop.ScopeName.local => Aesop.RuleIdent.fvar i.name

Instances For