inductive Aesop.BaseRuleSetMember : Type

• normRule: Aesop.NormRule → Aesop.BaseRuleSetMember
• unsafeRule: Aesop.UnsafeRule → Aesop.BaseRuleSetMember
• safeRule: Aesop.SafeRule → Aesop.BaseRuleSetMember
• unfoldRule: Aesop.UnfoldRule → Aesop.BaseRuleSetMember

instance Aesop.instInhabitedBaseRuleSetMember : Inhabited Aesop.BaseRuleSetMember

Equations

• Aesop.instInhabitedBaseRuleSetMember = { default := Aesop.BaseRuleSetMember.normRule default }

def Aesop.BaseRuleSetMember.name : Aesop.BaseRuleSetMember → Aesop.RuleName

Equations

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

inductive Aesop.GlobalRuleSetMember : Type

• base: Aesop.BaseRuleSetMember → Aesop.GlobalRuleSetMember
• normSimpRule: Aesop.NormSimpRule → Aesop.GlobalRuleSetMember

instance Aesop.instInhabitedGlobalRuleSetMember : Inhabited Aesop.GlobalRuleSetMember

Equations

• Aesop.instInhabitedGlobalRuleSetMember = { default := Aesop.GlobalRuleSetMember.base default }

def Aesop.GlobalRuleSetMember.name : Aesop.GlobalRuleSetMember → Aesop.RuleName

Equations

• Aesop.GlobalRuleSetMember.name x = match x with | Aesop.GlobalRuleSetMember.base m => Aesop.BaseRuleSetMember.name m | Aesop.GlobalRuleSetMember.normSimpRule r => r.name

inductive Aesop.LocalRuleSetMember : Type

• global: Aesop.GlobalRuleSetMember → Aesop.LocalRuleSetMember
• localNormSimpRule: Aesop.LocalNormSimpRule → Aesop.LocalRuleSetMember

instance Aesop.instInhabitedLocalRuleSetMember : Inhabited Aesop.LocalRuleSetMember

Equations

• Aesop.instInhabitedLocalRuleSetMember = { default := Aesop.LocalRuleSetMember.global default }

def Aesop.LocalRuleSetMember.name : Aesop.LocalRuleSetMember → Aesop.RuleName

Equations

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

def Aesop.LocalRuleSetMember.toGlobalRuleSetMember? : Aesop.LocalRuleSetMember → Option Aesop.GlobalRuleSetMember

Equations

• Aesop.LocalRuleSetMember.toGlobalRuleSetMember? x = match x with | Aesop.LocalRuleSetMember.global m => some m | x => none

structure Aesop.RuleNameFilter : Type

• ident : Aesop.RuleIdent
• builders : Array Aesop.BuilderName
• phases : Array Aesop.PhaseName

def Aesop.RuleNameFilter.ofIdent (i : Aesop.RuleIdent) : Aesop.RuleNameFilter

Equations

• Aesop.RuleNameFilter.ofIdent i = { ident := i, builders := #[], phases := #[] }

def Aesop.RuleNameFilter.matchesPhase (f : Aesop.RuleNameFilter) (p : Aesop.PhaseName) : Bool

Equations

• Aesop.RuleNameFilter.matchesPhase f p = (Array.isEmpty f.phases || Array.contains f.phases p)

def Aesop.RuleNameFilter.matchesBuilder (f : Aesop.RuleNameFilter) (b : Aesop.BuilderName) : Bool

Equations

• Aesop.RuleNameFilter.matchesBuilder f b = (Array.isEmpty f.builders || Array.contains f.builders b)

def Aesop.RuleNameFilter.matches (f : Aesop.RuleNameFilter) (n : Aesop.RuleName) : Bool

Equations

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

def Aesop.RuleNameFilter.matchesSimpTheorem? (f : Aesop.RuleNameFilter) : Option Lean.Name

Equations

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

def Aesop.RuleNameFilter.matchesLocalNormSimpRule? (f : Aesop.RuleNameFilter) : Option Aesop.LocalNormSimpRule

Equations

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

@[inline, reducible]

abbrev Aesop.RuleSetName : Type

Equations

• Aesop.RuleSetName = Lean.Name

def Aesop.defaultRuleSetName : Aesop.RuleSetName

Equations

• Aesop.defaultRuleSetName = `default

def Aesop.builtinRuleSetName : Aesop.RuleSetName

Equations

• Aesop.builtinRuleSetName = `builtin

def Aesop.localRuleSetName : Aesop.RuleSetName

Equations

• Aesop.localRuleSetName = `local

def Aesop.builtinRuleSetNames : Array Aesop.RuleSetName

Equations

• Aesop.builtinRuleSetNames = #[Aesop.defaultRuleSetName, Aesop.builtinRuleSetName]

def Aesop.RuleSetName.isReserved (n : Aesop.RuleSetName) : Bool

Equations

• Aesop.RuleSetName.isReserved n = (n == Aesop.localRuleSetName || Array.contains Aesop.builtinRuleSetNames n)

structure Aesop.RuleSetNameFilter : Type

• ns : Array Aesop.RuleSetName

def Aesop.RuleSetNameFilter.all : Aesop.RuleSetNameFilter

Equations

• Aesop.RuleSetNameFilter.all = { ns := #[] }

def Aesop.RuleSetNameFilter.matchesAll (f : Aesop.RuleSetNameFilter) : Bool

Equations

• Aesop.RuleSetNameFilter.matchesAll f = Array.isEmpty f.ns

def Aesop.RuleSetNameFilter.matches (f : Aesop.RuleSetNameFilter) (n : Aesop.RuleSetName) : Bool

Equations

• Aesop.RuleSetNameFilter.matches f n = (Aesop.RuleSetNameFilter.matchesAll f || Array.contains f.ns n)

def Aesop.RuleSetNameFilter.matchedRuleSetNames (f : Aesop.RuleSetNameFilter) : Option (Array Aesop.RuleSetName)

Equations

• Aesop.RuleSetNameFilter.matchedRuleSetNames f = if Aesop.RuleSetNameFilter.matchesAll f = true then none else some f.ns

structure Aesop.BaseRuleSet : Type

The Aesop-specific parts of an Aesop rule set. A BaseRuleSet stores global Aesop rules, e.g. safe and unsafe rules. It does not store simp theorems for the builtin norm simp rule; these are instead stored in a simp extension.

• normRules : Aesop.Index Aesop.NormRuleInfo

  Normalisation rules registered in this rule set.

• unsafeRules : Aesop.Index Aesop.UnsafeRuleInfo

  Unsafe rules registered in this rule set.

• safeRules : Aesop.Index Aesop.SafeRuleInfo

  Safe rules registered in this rule set.

• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)

  Rules for the builtin unfold rule. A pair (decl, unfoldThm?) in this map represents a declaration decl which should be unfolded. unfoldThm? should be the output of getUnfoldEqnFor? decl and is cached here for efficiency.

• erased : Lean.PHashSet Aesop.RuleName

  The set of rules that were erased from normRules, unsafeRules and safeRules. When we erase a rule which is present in any of these three indices, the rule is not removed from the indices but just added to this set. By contrast, when we erase a rule from unfoldRules, we actually delete it.

• ruleNames : Lean.PHashMap Aesop.RuleIdent (Aesop.UnorderedArraySet Aesop.RuleName)

  A cache of the names of all rules registered in this rule set. Invariant: ruleNames contains exactly the names of the rules present in normRules, unsafeRules, safeRules and unfoldRules and not present in erased. We use this cache (a) to quickly determine whether a rule is present in the rule set and (b) to find the full rule names corresponding to a RuleIdent.

instance Aesop.instInhabitedBaseRuleSet : Inhabited Aesop.BaseRuleSet

Equations

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

structure Aesop.GlobalRuleSetextends Aesop.BaseRuleSet : Type

A global Aesop rule set. When we tag a declaration with @[aesop], it is stored in one or more of these rule sets. Internally, a GlobalRuleSet is composed of a BaseRuleSet (stored in an Aesop rule set extension) plus a set of simp theorems (stored in a SimpExtension).

• normRules : Aesop.Index Aesop.NormRuleInfo
• unsafeRules : Aesop.Index Aesop.UnsafeRuleInfo
• safeRules : Aesop.Index Aesop.SafeRuleInfo
• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)
• erased : Lean.PHashSet Aesop.RuleName
• ruleNames : Lean.PHashMap Aesop.RuleIdent (Aesop.UnorderedArraySet Aesop.RuleName)
• simpTheorems : Lean.Meta.SimpTheorems

  The simp theorems stored in this rule set.

• simprocs : Lean.Meta.Simprocs

  The simprocs stored in this rule set.

instance Aesop.instInhabitedGlobalRuleSet : Inhabited Aesop.GlobalRuleSet

Equations

• Aesop.instInhabitedGlobalRuleSet = { default := { toBaseRuleSet := default, simpTheorems := default, simprocs := default } }

structure Aesop.LocalRuleSetextends Aesop.BaseRuleSet : Type

The rule set used by an Aesop tactic call. A local rule set is produced by combining several global rule sets and possibly adding or erasing some individual rules.

• normRules : Aesop.Index Aesop.NormRuleInfo
• unsafeRules : Aesop.Index Aesop.UnsafeRuleInfo
• safeRules : Aesop.Index Aesop.SafeRuleInfo
• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)
• erased : Lean.PHashSet Aesop.RuleName
• ruleNames : Lean.PHashMap Aesop.RuleIdent (Aesop.UnorderedArraySet Aesop.RuleName)
• simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems)

  The simp theorems used by the builtin norm simp rule.

• simpTheoremsArrayNonempty : 0 < Array.size self.simpTheoremsArray

  The simp theorems array must contain at least one SimpTheorems structure. When a simp theorem is added to a LocalRuleSet, it is stored in this first SimpTheorems structure.

• simprocsArray : Array (Lean.Name × Lean.Meta.Simprocs)

  The simprocs used by the builtin norm simp rule.

• simprocsArrayNonempty : 0 < Array.size self.simprocsArray

  The simprocs array must contain at least one Simprocs structure, for the same reason as above.

• localNormSimpRules : Array Aesop.LocalNormSimpRule

  FVars that were explicitly added as simp rules.

@[always_inline]

def Aesop.GlobalRuleSet.onBaseM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : Aesop.BaseRuleSet → m (Aesop.BaseRuleSet × α)) (rs : Aesop.GlobalRuleSet) : m (Aesop.GlobalRuleSet × α)

Equations

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

@[always_inline]

def Aesop.GlobalRuleSet.onBase {α : Type u_1} (f : Aesop.BaseRuleSet → Aesop.BaseRuleSet × α) (rs : Aesop.GlobalRuleSet) : Aesop.GlobalRuleSet × α

Equations

• Aesop.GlobalRuleSet.onBase f rs = Aesop.GlobalRuleSet.onBaseM f rs

@[always_inline]

def Aesop.GlobalRuleSet.modifyBaseM {m : Type → Type u_1} [Monad m] (f : Aesop.BaseRuleSet → m Aesop.BaseRuleSet) (rs : Aesop.GlobalRuleSet) : m Aesop.GlobalRuleSet

Equations

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

@[always_inline]

def Aesop.GlobalRuleSet.modifyBase (f : Aesop.BaseRuleSet → Aesop.BaseRuleSet) (rs : Aesop.GlobalRuleSet) : Aesop.GlobalRuleSet

Equations

• Aesop.GlobalRuleSet.modifyBase f rs = Aesop.GlobalRuleSet.modifyBaseM f rs

@[always_inline]

def Aesop.LocalRuleSet.onBaseM {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] (f : Aesop.BaseRuleSet → m (Aesop.BaseRuleSet × α)) (rs : Aesop.LocalRuleSet) : m (Aesop.LocalRuleSet × α)

Equations

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

@[always_inline]

def Aesop.LocalRuleSet.onBase {α : Type u_1} (f : Aesop.BaseRuleSet → Aesop.BaseRuleSet × α) (rs : Aesop.LocalRuleSet) : Aesop.LocalRuleSet × α

Equations

• Aesop.LocalRuleSet.onBase f rs = Aesop.LocalRuleSet.onBaseM f rs

def Aesop.LocalRuleSet.modifyBaseM {m : Type → Type u_1} [Monad m] (f : Aesop.BaseRuleSet → m Aesop.BaseRuleSet) (rs : Aesop.LocalRuleSet) : m Aesop.LocalRuleSet

Equations

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

def Aesop.LocalRuleSet.modifyBase (f : Aesop.BaseRuleSet → Aesop.BaseRuleSet) (rs : Aesop.LocalRuleSet) : Aesop.LocalRuleSet

Equations

• Aesop.LocalRuleSet.modifyBase f rs = Aesop.LocalRuleSet.modifyBaseM f rs

def Aesop.BaseRuleSet.trace (rs : Aesop.BaseRuleSet) (traceOpt : Aesop.TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.GlobalRuleSet.trace (rs : Aesop.GlobalRuleSet) (traceOpt : Aesop.TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.LocalRuleSet.trace (rs : Aesop.LocalRuleSet) (traceOpt : Aesop.TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.LocalRuleSet.trace.printSimpSetName : Lean.Name → String

Equations

• Aesop.LocalRuleSet.trace.printSimpSetName x = match x with | `_ => "<default>" | n => toString n

def Aesop.BaseRuleSet.empty : Aesop.BaseRuleSet

Equations

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

instance Aesop.instEmptyCollectionBaseRuleSet : EmptyCollection Aesop.BaseRuleSet

Equations

• Aesop.instEmptyCollectionBaseRuleSet = { emptyCollection := Aesop.BaseRuleSet.empty }

def Aesop.GlobalRuleSet.empty : Aesop.GlobalRuleSet

Equations

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

instance Aesop.instEmptyCollectionGlobalRuleSet : EmptyCollection Aesop.GlobalRuleSet

Equations

• Aesop.instEmptyCollectionGlobalRuleSet = { emptyCollection := Aesop.GlobalRuleSet.empty }

def Aesop.LocalRuleSet.empty : Aesop.LocalRuleSet

Equations

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

instance Aesop.instEmptyCollectionLocalRuleSet : EmptyCollection Aesop.LocalRuleSet

Equations

• Aesop.instEmptyCollectionLocalRuleSet = { emptyCollection := Aesop.LocalRuleSet.empty }

instance Aesop.instInhabitedLocalRuleSet : Inhabited Aesop.LocalRuleSet

Equations

• Aesop.instInhabitedLocalRuleSet = { default := ∅ }

def Aesop.BaseRuleSet.contains (rs : Aesop.BaseRuleSet) (n : Aesop.RuleName) : Bool

Equations

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

def Aesop.GlobalRuleSet.contains (rs : Aesop.GlobalRuleSet) (n : Aesop.RuleName) : Bool

Equations

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

def Aesop.LocalRuleSet.containsGlobalSimpTheorem (rs : Aesop.LocalRuleSet) (decl : Lean.Name) : Bool

Equations

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

def Aesop.LocalRuleSet.contains (rs : Aesop.LocalRuleSet) (n : Aesop.RuleName) : Bool

Equations

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

def Aesop.BaseRuleSet.merge (rs₁ : Aesop.BaseRuleSet) (rs₂ : Aesop.BaseRuleSet) : Aesop.BaseRuleSet

Equations

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

def Aesop.BaseRuleSet.add (rs : Aesop.BaseRuleSet) (r : Aesop.BaseRuleSetMember) : Aesop.BaseRuleSet

Equations

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

def Aesop.LocalRuleSet.add (rs : Aesop.LocalRuleSet) : Aesop.LocalRuleSetMember → Aesop.LocalRuleSet

Equations

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

def Aesop.BaseRuleSet.erase (rs : Aesop.BaseRuleSet) (f : Aesop.RuleNameFilter) : Aesop.BaseRuleSet × Bool

Equations

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

def Aesop.GlobalRuleSet.erase (rs : Aesop.GlobalRuleSet) (f : Aesop.RuleNameFilter) : Aesop.GlobalRuleSet × Bool

Equations

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

def Aesop.LocalRuleSet.erase (rs : Aesop.LocalRuleSet) (f : Aesop.RuleNameFilter) : Aesop.LocalRuleSet × Bool

Equations

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

def Aesop.LocalRuleSet.applicableNormalizationRules (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) : Lean.MetaM (Array (Aesop.IndexMatchResult Aesop.NormRule))

Equations

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

def Aesop.LocalRuleSet.applicableUnsafeRules (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) : Lean.MetaM (Array (Aesop.IndexMatchResult Aesop.UnsafeRule))

Equations

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

def Aesop.LocalRuleSet.applicableSafeRules (rs : Aesop.LocalRuleSet) (goal : Lean.MVarId) : Lean.MetaM (Array (Aesop.IndexMatchResult Aesop.SafeRule))

Equations

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

def Aesop.LocalRuleSet.unindex (rs : Aesop.LocalRuleSet) (p : Aesop.RuleName → Bool) : Aesop.LocalRuleSet

Equations

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

@[always_inline]

def Aesop.unindexPredicate? (options : Aesop.Options') : Option (Aesop.RuleName → Bool)

Equations

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

def Aesop.mkLocalRuleSet (rss : Array (Aesop.GlobalRuleSet × Lean.Name × Lean.Name)) (options : Aesop.Options') : Lean.CoreM Aesop.LocalRuleSet

Equations

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