Normalisation Rules

structure Aesop.NormRuleInfo : Type

• penalty : Int

Instances For

• Aesop.instInhabitedNormRuleInfo
• Aesop.instLENormRuleInfo
• Aesop.instLTNormRuleInfo
• Aesop.instOrdNormRuleInfo

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 => 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

@[inline, reducible]

abbrev Aesop.NormRule : Type

Equations

• Aesop.NormRule = Aesop.Rule Aesop.NormRuleInfo

Instances For

• Aesop.instToStringNormRule

instance Aesop.instToStringNormRule : ToString Aesop.NormRule

Equations

• Aesop.instToStringNormRule = { toString := fun r => 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

Instances For

• Aesop.Safety.instToStringSafety
• Aesop.instInhabitedSafety

instance Aesop.instInhabitedSafety : Inhabited Aesop.Safety

Equations

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

instance Aesop.Safety.instToStringSafety : ToString Aesop.Safety

Equations

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

structure Aesop.SafeRuleInfo : Type

• penalty : Int
• safety : Aesop.Safety

Instances For

• Aesop.instInhabitedSafeRuleInfo
• Aesop.instLESafeRuleInfo
• Aesop.instLTSafeRuleInfo
• Aesop.instOrdSafeRuleInfo

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 => 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

@[inline, reducible]

abbrev Aesop.SafeRule : Type

Equations

• Aesop.SafeRule = Aesop.Rule Aesop.SafeRuleInfo

Instances For

• Aesop.instToStringSafeRule

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

Instances For

• Aesop.instInhabitedUnsafeRuleInfo
• Aesop.instLEUnsafeRuleInfo
• Aesop.instLTUnsafeRuleInfo
• Aesop.instOrdUnsafeRuleInfo

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 => 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

@[inline, reducible]

abbrev Aesop.UnsafeRule : Type

Equations

• Aesop.UnsafeRule = Aesop.Rule Aesop.UnsafeRuleInfo

Instances For

• Aesop.instToStringUnsafeRule

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

Instances For

• Aesop.RegularRule.instToFormatRegularRule
• Aesop.instBEqRegularRule
• Aesop.instInhabitedRegularRule

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.instToFormatRegularRule : Lean.ToFormat Aesop.RegularRule

Equations

• Aesop.RegularRule.instToFormatRegularRule = { format := fun x => match x with | Aesop.RegularRule.safe r => Std.format r | Aesop.RegularRule.unsafe r => Std.format r }

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

Equations

• Aesop.RegularRule.successProbability x = match x with | Aesop.RegularRule.safe r => Aesop.Percent.hundred | Aesop.RegularRule.unsafe r => r.extra.successProbability

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

Equations

• Aesop.RegularRule.isSafe x = match x with | Aesop.RegularRule.safe r => true | Aesop.RegularRule.unsafe r => false

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

Equations

• Aesop.RegularRule.isUnsafe x = match x with | Aesop.RegularRule.safe r => false | Aesop.RegularRule.unsafe r => true

@[inline]

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

Equations

• Aesop.RegularRule.withRule f x = match x with | Aesop.RegularRule.safe r => f Aesop.SafeRuleInfo r | Aesop.RegularRule.unsafe r => f Aesop.UnsafeRuleInfo r

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

Equations

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

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

Equations

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

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

Equations

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

Normalisation Simp Rules

structure Aesop.NormSimpRule : Type

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

Instances For

• Aesop.LocalNormSimpRule.instBEqNormSimpRule
• Aesop.LocalNormSimpRule.instHashableNormSimpRule
• Aesop.NormSimpRule.instBEqNormSimpRule
• Aesop.NormSimpRule.instHashableNormSimpRule
• Aesop.instInhabitedNormSimpRule

instance Aesop.instInhabitedNormSimpRule : Inhabited Aesop.NormSimpRule

Equations

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

instance Aesop.NormSimpRule.instBEqNormSimpRule : BEq Aesop.NormSimpRule

Equations

• Aesop.NormSimpRule.instBEqNormSimpRule = { beq := fun r s => r.name == s.name }

instance Aesop.NormSimpRule.instHashableNormSimpRule : Hashable Aesop.NormSimpRule

Equations

• Aesop.NormSimpRule.instHashableNormSimpRule = { hash := fun r => hash r.name }

structure Aesop.LocalNormSimpRule : Type

• fvarUserName : Lean.Name

Instances For

• Aesop.instInhabitedLocalNormSimpRule

instance Aesop.instInhabitedLocalNormSimpRule : Inhabited Aesop.LocalNormSimpRule

Equations

• Aesop.instInhabitedLocalNormSimpRule = { default := { fvarUserName := default } }

instance Aesop.LocalNormSimpRule.instBEqNormSimpRule : BEq Aesop.NormSimpRule

Equations

• Aesop.LocalNormSimpRule.instBEqNormSimpRule = { beq := fun r s => r.name == s.name }

instance Aesop.LocalNormSimpRule.instHashableNormSimpRule : Hashable Aesop.NormSimpRule

Equations

• Aesop.LocalNormSimpRule.instHashableNormSimpRule = { hash := fun r => hash r.name }

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

Instances For

• Aesop.UnfoldRule.instBEqUnfoldRule
• Aesop.UnfoldRule.instHashableUnfoldRule
• Aesop.instInhabitedUnfoldRule

instance Aesop.instInhabitedUnfoldRule : Inhabited Aesop.UnfoldRule

Equations

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

instance Aesop.UnfoldRule.instBEqUnfoldRule : BEq Aesop.UnfoldRule

Equations

• Aesop.UnfoldRule.instBEqUnfoldRule = { beq := fun r s => r.decl == s.decl }

instance Aesop.UnfoldRule.instHashableUnfoldRule : Hashable Aesop.UnfoldRule

Equations

• Aesop.UnfoldRule.instHashableUnfoldRule = { hash := fun r => 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.