inductive Aesop.PhaseName : Type

• norm : PhaseName
• safe : PhaseName
• unsafe : PhaseName

def Aesop.instInhabitedPhaseName.default : PhaseName

instance Aesop.instInhabitedPhaseName : Inhabited PhaseName

def Aesop.instBEqPhaseName.beq : PhaseName → PhaseName → Bool

instance Aesop.instBEqPhaseName : BEq PhaseName

instance Aesop.instHashablePhaseName : Hashable PhaseName

def Aesop.instHashablePhaseName.hash : PhaseName → UInt64

def Aesop.instToJsonPhaseName.toJson : PhaseName → Lean.Json

instance Aesop.instToJsonPhaseName : Lean.ToJson PhaseName

instance Aesop.PhaseName.instOrd : Ord PhaseName

instance Aesop.PhaseName.instToString : ToString PhaseName

inductive Aesop.ScopeName : Type

• global : ScopeName
• local : ScopeName

instance Aesop.instInhabitedScopeName : Inhabited ScopeName

def Aesop.instInhabitedScopeName.default : ScopeName

instance Aesop.instBEqScopeName : BEq ScopeName

def Aesop.instBEqScopeName.beq : ScopeName → ScopeName → Bool

instance Aesop.instHashableScopeName : Hashable ScopeName

def Aesop.instHashableScopeName.hash : ScopeName → UInt64

def Aesop.instToJsonScopeName.toJson : ScopeName → Lean.Json

instance Aesop.instToJsonScopeName : Lean.ToJson ScopeName

instance Aesop.ScopeName.instOrd : Ord ScopeName

instance Aesop.ScopeName.instToString : ToString ScopeName

inductive Aesop.BuilderName : Type

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

instance Aesop.instInhabitedBuilderName : Inhabited BuilderName

def Aesop.instInhabitedBuilderName.default : BuilderName

instance Aesop.instBEqBuilderName : BEq BuilderName

def Aesop.instBEqBuilderName.beq : BuilderName → BuilderName → Bool

instance Aesop.instHashableBuilderName : Hashable BuilderName

def Aesop.instHashableBuilderName.hash : BuilderName → UInt64

def Aesop.instToJsonBuilderName.toJson : BuilderName → Lean.Json

instance Aesop.instToJsonBuilderName : Lean.ToJson BuilderName

instance Aesop.BuilderName.instOrd : Ord BuilderName

instance Aesop.BuilderName.instToString : ToString BuilderName

structure Aesop.RuleName : Type

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

def Aesop.instInhabitedRuleName.default : RuleName

instance Aesop.instInhabitedRuleName : Inhabited RuleName

instance Aesop.RuleName.instHashable : Hashable RuleName

instance Aesop.RuleName.instBEq : BEq RuleName

def Aesop.RuleName.compare : RuleName → RuleName → Ordering

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

instance Aesop.RuleName.instOrd : Ord RuleName

instance Aesop.RuleName.instToString : ToString RuleName

instance Aesop.RuleName.instToJson : Lean.ToJson RuleName

def Aesop.getRuleNameForExpr : Lean.Expr → Lean.MetaM Lean.Name

inductive Aesop.DisplayRuleName : Type

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

instance Aesop.instInhabitedDisplayRuleName : Inhabited DisplayRuleName

def Aesop.instInhabitedDisplayRuleName.default : DisplayRuleName

instance Aesop.instBEqDisplayRuleName : BEq DisplayRuleName

def Aesop.instBEqDisplayRuleName.beq : DisplayRuleName → DisplayRuleName → Bool

instance Aesop.instOrdDisplayRuleName : Ord DisplayRuleName

def Aesop.instOrdDisplayRuleName.ord : DisplayRuleName → DisplayRuleName → Ordering

instance Aesop.instHashableDisplayRuleName : Hashable DisplayRuleName

def Aesop.instHashableDisplayRuleName.hash : DisplayRuleName → UInt64

instance Aesop.DisplayRuleName.instCoeRuleName : Coe RuleName DisplayRuleName

instance Aesop.DisplayRuleName.instToString : ToString DisplayRuleName

instance Aesop.DisplayRuleName.instToJson : Lean.ToJson DisplayRuleName