Normalisation Rules

structure Aesop.NormRuleInfo : Type

• penalty : Int

instance Aesop.instInhabitedNormRuleInfo : Inhabited Aesop.NormRuleInfo

Equations

• Aesop.instInhabitedNormRuleInfo = { default := { penalty := default } }

instance Aesop.instOrdNormRuleInfo : Ord Aesop.NormRuleInfo

Equations

• Aesop.instOrdNormRuleInfo = { compare := fun (i j : Aesop.NormRuleInfo) => compare i.penalty j.penalty }

instance Aesop.instLTNormRuleInfo : LT Aesop.NormRuleInfo

Equations

• Aesop.instLTNormRuleInfo = ltOfOrd

instance Aesop.instLENormRuleInfo : LE Aesop.NormRuleInfo

Equations

• Aesop.instLENormRuleInfo = leOfOrd

@[reducible, inline]

abbrev Aesop.NormRule : Type

Equations

• Aesop.NormRule = Aesop.Rule Aesop.NormRuleInfo

instance Aesop.instToStringNormRule : ToString Aesop.NormRule

Equations

• Aesop.instToStringNormRule = { toString := fun (r : Aesop.NormRule) => toString "[" ++ toString r.extra.penalty ++ toString "] " ++ toString r.name ++ toString "" }

def Aesop.defaultNormPenalty : Int

Equations

• Aesop.defaultNormPenalty = 1

def Aesop.defaultSimpRulePriority : Int

Equations

• Aesop.defaultSimpRulePriority = 1000

Safe and Almost Safe Rules

inductive Aesop.Safety : Type

• safe: Aesop.Safety
• almostSafe: Aesop.Safety

instance Aesop.instInhabitedSafety : Inhabited Aesop.Safety

Equations

• Aesop.instInhabitedSafety = { default := Aesop.Safety.safe }

instance Aesop.Safety.instToString : ToString Aesop.Safety

Equations

• Aesop.Safety.instToString = { toString := fun (x : Aesop.Safety) => match x with | Aesop.Safety.safe => "safe" | Aesop.Safety.almostSafe => "almostSafe" }

structure Aesop.SafeRuleInfo : Type

• penalty : Int
• safety : Aesop.Safety

instance Aesop.instInhabitedSafeRuleInfo : Inhabited Aesop.SafeRuleInfo

Equations

• Aesop.instInhabitedSafeRuleInfo = { default := { penalty := default, safety := default } }

instance Aesop.instOrdSafeRuleInfo : Ord Aesop.SafeRuleInfo

Equations

• Aesop.instOrdSafeRuleInfo = { compare := fun (i j : Aesop.SafeRuleInfo) => compare i.penalty j.penalty }

instance Aesop.instLTSafeRuleInfo : LT Aesop.SafeRuleInfo

Equations

• Aesop.instLTSafeRuleInfo = ltOfOrd

instance Aesop.instLESafeRuleInfo : LE Aesop.SafeRuleInfo

Equations

• Aesop.instLESafeRuleInfo = leOfOrd

@[reducible, inline]

abbrev Aesop.SafeRule : Type

Equations

• Aesop.SafeRule = Aesop.Rule Aesop.SafeRuleInfo

instance Aesop.instToStringSafeRule : ToString Aesop.SafeRule

Equations

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

def Aesop.defaultSafePenalty : Int

Equations

• Aesop.defaultSafePenalty = 1

Unsafe Rules

structure Aesop.UnsafeRuleInfo : Type

• successProbability : Aesop.Percent

instance Aesop.instInhabitedUnsafeRuleInfo : Inhabited Aesop.UnsafeRuleInfo

Equations

• Aesop.instInhabitedUnsafeRuleInfo = { default := { successProbability := default } }

instance Aesop.instOrdUnsafeRuleInfo : Ord Aesop.UnsafeRuleInfo

Equations

• Aesop.instOrdUnsafeRuleInfo = { compare := fun (i j : Aesop.UnsafeRuleInfo) => compare j.successProbability i.successProbability }

instance Aesop.instLTUnsafeRuleInfo : LT Aesop.UnsafeRuleInfo

Equations

• Aesop.instLTUnsafeRuleInfo = ltOfOrd

instance Aesop.instLEUnsafeRuleInfo : LE Aesop.UnsafeRuleInfo

Equations

• Aesop.instLEUnsafeRuleInfo = leOfOrd

@[reducible, inline]

abbrev Aesop.UnsafeRule : Type

Equations

• Aesop.UnsafeRule = Aesop.Rule Aesop.UnsafeRuleInfo

instance Aesop.instToStringUnsafeRule : ToString Aesop.UnsafeRule

Equations

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

def Aesop.defaultSuccessProbability : Aesop.Percent

Equations

• Aesop.defaultSuccessProbability = Aesop.Percent.fifty

Regular Rules

inductive Aesop.RegularRule : Type

• safe: Aesop.SafeRule → Aesop.RegularRule
• unsafe: Aesop.UnsafeRule → Aesop.RegularRule

instance Aesop.instInhabitedRegularRule : Inhabited Aesop.RegularRule

Equations

• Aesop.instInhabitedRegularRule = { default := Aesop.RegularRule.safe default }

instance Aesop.instBEqRegularRule : BEq Aesop.RegularRule

Equations

• Aesop.instBEqRegularRule = { beq := Aesop.beqRegularRule✝ }

instance Aesop.RegularRule.instToFormat : Lean.ToFormat Aesop.RegularRule

Equations

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

def Aesop.RegularRule.successProbability : Aesop.RegularRule → Aesop.Percent

Equations

• (Aesop.RegularRule.safe r).successProbability = Aesop.Percent.hundred
• (Aesop.RegularRule.unsafe r).successProbability = r.extra.successProbability

def Aesop.RegularRule.isSafe : Aesop.RegularRule → Bool

Equations

• (Aesop.RegularRule.safe r).isSafe = true
• (Aesop.RegularRule.unsafe r).isSafe = false

def Aesop.RegularRule.isUnsafe : Aesop.RegularRule → Bool

Equations

• (Aesop.RegularRule.safe r).isUnsafe = false
• (Aesop.RegularRule.unsafe r).isUnsafe = true

@[inline]

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

Equations

• Aesop.RegularRule.withRule f (Aesop.RegularRule.safe r) = f r
• Aesop.RegularRule.withRule f (Aesop.RegularRule.unsafe r) = f r

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

Equations

• r.name = Aesop.RegularRule.withRule (fun {α : Type} (x : Aesop.Rule α) => x.name) r

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

Equations

• r.indexingMode = Aesop.RegularRule.withRule (fun {α : Type} (x : Aesop.Rule α) => x.indexingMode) r

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

Equations

• r.tac = Aesop.RegularRule.withRule (fun {α : Type} (x : Aesop.Rule α) => x.tac) r

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 : Aesop.RuleName
• entries : Array Lean.Meta.SimpEntry

instance Aesop.instInhabitedNormSimpRule : Inhabited Aesop.NormSimpRule

Equations

• Aesop.instInhabitedNormSimpRule = { default := { name := default, entries := default } }

instance Aesop.NormSimpRule.instBEq : BEq Aesop.NormSimpRule

Equations

• Aesop.NormSimpRule.instBEq = { beq := fun (r s : Aesop.NormSimpRule) => r.name == s.name }

instance Aesop.NormSimpRule.instHashable : Hashable Aesop.NormSimpRule

Equations

• Aesop.NormSimpRule.instHashable = { hash := fun (r : Aesop.NormSimpRule) => hash r.name }

structure Aesop.LocalNormSimpRule : Type

A local rule for the norm simplifier.

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

instance Aesop.instInhabitedLocalNormSimpRule : Inhabited Aesop.LocalNormSimpRule

Equations

• Aesop.instInhabitedLocalNormSimpRule = { default := { id := default, simpTheorem := default } }

instance Aesop.LocalNormSimpRule.instBEq : BEq Aesop.LocalNormSimpRule

Equations

• Aesop.LocalNormSimpRule.instBEq = { beq := fun (r₁ r₂ : Aesop.LocalNormSimpRule) => r₁.id == r₂.id }

instance Aesop.LocalNormSimpRule.instHashable : Hashable Aesop.LocalNormSimpRule

Equations

• Aesop.LocalNormSimpRule.instHashable = { hash := fun (r : Aesop.LocalNormSimpRule) => hash r.id }

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

Equations

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

structure Aesop.UnfoldRule : Type

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

instance Aesop.instInhabitedUnfoldRule : Inhabited Aesop.UnfoldRule

Equations

• Aesop.instInhabitedUnfoldRule = { default := { decl := default, unfoldThm? := default } }

instance Aesop.UnfoldRule.instBEq : BEq Aesop.UnfoldRule

Equations

• Aesop.UnfoldRule.instBEq = { beq := fun (r s : Aesop.UnfoldRule) => r.decl == s.decl }

instance Aesop.UnfoldRule.instHashable : Hashable Aesop.UnfoldRule

Equations

• Aesop.UnfoldRule.instHashable = { hash := fun (r : Aesop.UnfoldRule) => hash r.decl }

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

Equations

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