Normalisation Rules

structure Aesop.NormRuleInfo : Type

• penalty : Int

@[implicit_reducible]

instance Aesop.instInhabitedNormRuleInfo : Inhabited NormRuleInfo

def Aesop.instInhabitedNormRuleInfo.default : NormRuleInfo

@[implicit_reducible]

instance Aesop.instOrdNormRuleInfo : Ord NormRuleInfo

@[implicit_reducible]

instance Aesop.instLTNormRuleInfo : LT NormRuleInfo

@[implicit_reducible]

instance Aesop.instLENormRuleInfo : LE NormRuleInfo

@[reducible, inline]

abbrev Aesop.NormRule : Type

@[implicit_reducible]

instance Aesop.instToStringNormRule : ToString NormRule

def Aesop.defaultNormPenalty : Int

def Aesop.defaultSimpRulePriority : Int

Safe and Almost Safe Rules

inductive Aesop.Safety : Type

• safe : Safety
• almostSafe : Safety

@[implicit_reducible]

instance Aesop.instInhabitedSafety : Inhabited Safety

def Aesop.instInhabitedSafety.default : Safety

@[implicit_reducible]

instance Aesop.Safety.instToString : ToString Safety

structure Aesop.SafeRuleInfo : Type

• penalty : Int
• safety : Safety

def Aesop.instInhabitedSafeRuleInfo.default : SafeRuleInfo

@[implicit_reducible]

instance Aesop.instInhabitedSafeRuleInfo : Inhabited SafeRuleInfo

@[implicit_reducible]

instance Aesop.instOrdSafeRuleInfo : Ord SafeRuleInfo

@[implicit_reducible]

instance Aesop.instLTSafeRuleInfo : LT SafeRuleInfo

@[implicit_reducible]

instance Aesop.instLESafeRuleInfo : LE SafeRuleInfo

@[reducible, inline]

abbrev Aesop.SafeRule : Type

@[implicit_reducible]

instance Aesop.instToStringSafeRule : ToString SafeRule

def Aesop.defaultSafePenalty : Int

Unsafe Rules

structure Aesop.UnsafeRuleInfo : Type

• successProbability : Percent

@[implicit_reducible]

instance Aesop.instInhabitedUnsafeRuleInfo : Inhabited UnsafeRuleInfo

def Aesop.instInhabitedUnsafeRuleInfo.default : UnsafeRuleInfo

@[implicit_reducible]

instance Aesop.instOrdUnsafeRuleInfo : Ord UnsafeRuleInfo

@[implicit_reducible]

instance Aesop.instLTUnsafeRuleInfo : LT UnsafeRuleInfo

@[implicit_reducible]

instance Aesop.instLEUnsafeRuleInfo : LE UnsafeRuleInfo

@[reducible, inline]

abbrev Aesop.UnsafeRule : Type

@[implicit_reducible]

instance Aesop.instToStringUnsafeRule : ToString UnsafeRule

def Aesop.defaultSuccessProbability : Percent

Regular Rules

inductive Aesop.RegularRule : Type

• safe (r : SafeRule) : RegularRule
• unsafe (r : UnsafeRule) : RegularRule

def Aesop.instInhabitedRegularRule.default : RegularRule

@[implicit_reducible]

instance Aesop.instInhabitedRegularRule : Inhabited RegularRule

def Aesop.instBEqRegularRule.beq : RegularRule → RegularRule → Bool

@[implicit_reducible]

instance Aesop.instBEqRegularRule : BEq RegularRule

@[implicit_reducible]

instance Aesop.RegularRule.instToFormat : Std.ToFormat RegularRule

def Aesop.RegularRule.successProbability : RegularRule → Percent

def Aesop.RegularRule.isSafe : RegularRule → Bool

def Aesop.RegularRule.isUnsafe : RegularRule → Bool

@[inline]

def Aesop.RegularRule.withRule {β : Sort u_1} (f : {α : Type} → Rule α → β) : RegularRule → β

def Aesop.RegularRule.name (r : RegularRule) : RuleName

def Aesop.RegularRule.indexingMode (r : RegularRule) : IndexingMode

def Aesop.RegularRule.tac (r : RegularRule) : RuleTacDescr

Normalisation Simp Rules

structure Aesop.NormSimpRule : Type

A global rule for the norm simplifier. Each SimpEntry represents a member of the simp set, e.g. a declaration whose type is an equality or a smart unfolding theorem for a declaration.

• name : RuleName
• entries : Array Lean.Meta.SimpEntry

@[implicit_reducible]

instance Aesop.instInhabitedNormSimpRule : Inhabited NormSimpRule

def Aesop.instInhabitedNormSimpRule.default : NormSimpRule

@[implicit_reducible]

instance Aesop.NormSimpRule.instBEq : BEq NormSimpRule

@[implicit_reducible]

instance Aesop.NormSimpRule.instHashable : Hashable NormSimpRule

structure Aesop.LocalNormSimpRule : Type

A local rule for the norm simplifier.

• id : Lean.Name
• simpTheorem : Lean.Term

@[implicit_reducible]

instance Aesop.instInhabitedLocalNormSimpRule : Inhabited LocalNormSimpRule

def Aesop.instInhabitedLocalNormSimpRule.default : LocalNormSimpRule

@[implicit_reducible]

instance Aesop.LocalNormSimpRule.instBEq : BEq LocalNormSimpRule

@[implicit_reducible]

instance Aesop.LocalNormSimpRule.instHashable : Hashable LocalNormSimpRule

def Aesop.LocalNormSimpRule.name (r : LocalNormSimpRule) : RuleName

structure Aesop.UnfoldRule : Type

• decl : Lean.Name
• unfoldThm? : Option Lean.Name

@[implicit_reducible]

instance Aesop.instInhabitedUnfoldRule : Inhabited UnfoldRule

def Aesop.instInhabitedUnfoldRule.default : UnfoldRule

@[implicit_reducible]

instance Aesop.UnfoldRule.instBEq : BEq UnfoldRule

@[implicit_reducible]

instance Aesop.UnfoldRule.instHashable : Hashable UnfoldRule

def Aesop.UnfoldRule.name (r : UnfoldRule) : RuleName