Aesop.Rule.Name

source

inductive Aesop.PhaseName :

Type

norm : PhaseName
safe : PhaseName
unsafe : PhaseName

Instances For

source

def Aesop.instInhabitedPhaseName.default :

PhaseName

Instances For

source

@[implicit_reducible]

instance Aesop.instInhabitedPhaseName :

Inhabited PhaseName

source

def Aesop.instBEqPhaseName.beq :

PhaseName → PhaseName → Bool

Instances For

source

@[implicit_reducible]

instance Aesop.instBEqPhaseName :

BEq PhaseName

source

@[implicit_reducible]

instance Aesop.instHashablePhaseName :

Hashable PhaseName

source

def Aesop.instHashablePhaseName.hash :

PhaseName → UInt64

Instances For

source

def Aesop.instToJsonPhaseName.toJson :

PhaseName → Lean.Json

Instances For

source

@[implicit_reducible]

instance Aesop.instToJsonPhaseName :

Lean.ToJson PhaseName

source

@[implicit_reducible]

instance Aesop.PhaseName.instOrd :

Ord PhaseName

source

@[implicit_reducible]

instance Aesop.PhaseName.instToString :

ToString PhaseName

source

inductive Aesop.ScopeName :

Type

global : ScopeName
local : ScopeName

Instances For

source

@[implicit_reducible]

instance Aesop.instInhabitedScopeName :

Inhabited ScopeName

source

def Aesop.instInhabitedScopeName.default :

ScopeName

Instances For

source

@[implicit_reducible]

instance Aesop.instBEqScopeName :

BEq ScopeName

source

def Aesop.instBEqScopeName.beq :

ScopeName → ScopeName → Bool

Instances For

source

@[implicit_reducible]

instance Aesop.instHashableScopeName :

Hashable ScopeName

source

def Aesop.instHashableScopeName.hash :

ScopeName → UInt64

Instances For

source

def Aesop.instToJsonScopeName.toJson :

ScopeName → Lean.Json

Instances For

source

@[implicit_reducible]

instance Aesop.instToJsonScopeName :

Lean.ToJson ScopeName

source

@[implicit_reducible]

instance Aesop.ScopeName.instOrd :

Ord ScopeName

source

@[implicit_reducible]

instance Aesop.ScopeName.instToString :

ToString ScopeName

source

inductive Aesop.BuilderName :

Type

apply : BuilderName
cases : BuilderName
constructors : BuilderName
destruct : BuilderName
forward : BuilderName
simp : BuilderName
tactic : BuilderName
unfold : BuilderName

Instances For

source

@[implicit_reducible]

instance Aesop.instInhabitedBuilderName :

Inhabited BuilderName

source

def Aesop.instInhabitedBuilderName.default :

BuilderName

Instances For

source

@[implicit_reducible]

instance Aesop.instBEqBuilderName :

BEq BuilderName

source

def Aesop.instBEqBuilderName.beq :

BuilderName → BuilderName → Bool

Instances For

source

def Aesop.instHashableBuilderName.hash :

BuilderName → UInt64

Instances For

source

@[implicit_reducible]

instance Aesop.instHashableBuilderName :

Hashable BuilderName

source

def Aesop.instToJsonBuilderName.toJson :

BuilderName → Lean.Json

Instances For

source

@[implicit_reducible]

instance Aesop.instToJsonBuilderName :

Lean.ToJson BuilderName

source

@[implicit_reducible]

instance Aesop.BuilderName.instOrd :

Ord BuilderName

source

@[implicit_reducible]

instance Aesop.BuilderName.instToString :

ToString BuilderName

source

structure Aesop.RuleName :

Type

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

Instances For

source

@[implicit_reducible]

instance Aesop.instInhabitedRuleName :

Inhabited RuleName

source

def Aesop.instInhabitedRuleName.default :

RuleName

Instances For

source

@[implicit_reducible]

instance Aesop.RuleName.instHashable :

Hashable RuleName

source

@[implicit_reducible]

instance Aesop.RuleName.instBEq :

BEq RuleName

source

def Aesop.RuleName.compare :

RuleName → RuleName → Ordering

Instances For

source

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

Ordering

Instances For

source

@[implicit_reducible]

instance Aesop.RuleName.instOrd :

Ord RuleName

source

@[implicit_reducible]

instance Aesop.RuleName.instToString :

ToString RuleName

source

@[implicit_reducible]

instance Aesop.RuleName.instToJson :

Lean.ToJson RuleName

source

def Aesop.getRuleNameForExpr :

Lean.Expr → Lean.MetaM Lean.Name

Instances For

source

inductive Aesop.DisplayRuleName :

Type

ruleName (n : RuleName) : DisplayRuleName
normSimp : DisplayRuleName
normUnfold : DisplayRuleName

Instances For

source

@[implicit_reducible]

instance Aesop.instInhabitedDisplayRuleName :

Inhabited DisplayRuleName

source

def Aesop.instInhabitedDisplayRuleName.default :

DisplayRuleName

Instances For

source

def Aesop.instBEqDisplayRuleName.beq :

DisplayRuleName → DisplayRuleName → Bool

Instances For

source

@[implicit_reducible]

instance Aesop.instBEqDisplayRuleName :

BEq DisplayRuleName

source

def Aesop.instOrdDisplayRuleName.ord :

DisplayRuleName → DisplayRuleName → Ordering

Instances For

source

@[implicit_reducible]

instance Aesop.instOrdDisplayRuleName :

Ord DisplayRuleName

source

@[implicit_reducible]

instance Aesop.instHashableDisplayRuleName :

Hashable DisplayRuleName

source

def Aesop.instHashableDisplayRuleName.hash :

DisplayRuleName → UInt64

Instances For

source

@[implicit_reducible]

instance Aesop.DisplayRuleName.instCoeRuleName :

Coe RuleName DisplayRuleName

source

@[implicit_reducible]

instance Aesop.DisplayRuleName.instToString :

ToString DisplayRuleName

source

@[implicit_reducible]

instance Aesop.DisplayRuleName.instToJson :

Lean.ToJson DisplayRuleName