Documentation

Aesop.Rule

Normalisation Rules #

structure Aesop.NormRuleInfo :

penalty : Int

Instances For

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 :

Equations

Aesop.NormRule = Aesop.Rule Aesop.NormRuleInfo

Instances For

Aesop.instToStringNormRule

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 :

Equations

Aesop.defaultNormPenalty = 1

def Aesop.defaultSimpRulePriority :

Equations

Aesop.defaultSimpRulePriority = 1000

Safe and Almost Safe Rules #

inductive Aesop.Safety :

safe: Aesop.Safety
almostSafe: Aesop.Safety

Instances For

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 :

penalty : Int
safety : Aesop.Safety

Instances For

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 :

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 :

Equations

Aesop.defaultSafePenalty = 1

Unsafe Rules #

structure Aesop.UnsafeRuleInfo :

successProbability : Aesop.Percent

Instances For

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 :

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 :

Equations

Aesop.defaultSuccessProbability = Aesop.Percent.fifty

Regular Rules #

inductive Aesop.RegularRule :

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

Instances For

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

x.successProbability = 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

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

def Aesop.RegularRule.isUnsafe :

Aesop.RegularRule → Bool

Equations

x.isUnsafe = 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 r | Aesop.RegularRule.unsafe r => f r

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

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 :

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

Instances For

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 :

A local rule for the norm simplifier.

id : Lean.Name
simpTheorem : Lean.Term

Instances For

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) :

Equations

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

structure Aesop.UnfoldRule :

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

Instances For

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) :

Equations

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