inductive Aesop.PhaseName : Type

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

instance Aesop.instInhabitedPhaseName : Inhabited PhaseName

instance Aesop.instBEqPhaseName : BEq PhaseName

instance Aesop.instHashablePhaseName : Hashable 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

instance Aesop.instBEqScopeName : BEq ScopeName

instance Aesop.instHashableScopeName : Hashable 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

instance Aesop.instBEqBuilderName : BEq BuilderName

instance Aesop.instHashableBuilderName : Hashable 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

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

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

instance Aesop.instBEqDisplayRuleName : BEq DisplayRuleName

instance Aesop.instOrdDisplayRuleName : Ord DisplayRuleName

instance Aesop.instHashableDisplayRuleName : Hashable DisplayRuleName

instance Aesop.DisplayRuleName.instCoeRuleName : Coe RuleName DisplayRuleName

instance Aesop.DisplayRuleName.instToString : ToString DisplayRuleName