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 Lean.Name (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 associated with the fvar or const identified by a name.

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 Lean.Name (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 Lean.Name (Aesop.UnorderedArraySet Aesop.RuleName)
• simpTheoremsArray : Array (Lean.Name × Lean.Meta.SimpTheorems)

  The simp theorems used by the builtin norm simp rule.

• simpTheoremsArrayNonempty : 0 < self.simpTheoremsArray.size

  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 < self.simprocsArray.size

  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.

theorem Aesop.LocalRuleSet.simpTheoremsArrayNonempty (self : Aesop.LocalRuleSet) : 0 < self.simpTheoremsArray.size

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.

theorem Aesop.LocalRuleSet.simprocsArrayNonempty (self : Aesop.LocalRuleSet) : 0 < self.simprocsArray.size

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

@[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

• rs.contains n = (rs.contains n || n.builder == Aesop.BuilderName.simp && n.scope == Aesop.ScopeName.global && Aesop.SimpTheorems.containsDecl rs.simpTheorems n.name)

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

• rs.applicableNormalizationRules goal = rs.normRules.applicableRules goal fun (x : Aesop.Rule Aesop.NormRuleInfo) => !Aesop.BaseRuleSet.isErased rs.toBaseRuleSet x.name

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

Equations

• rs.applicableUnsafeRules goal = rs.unsafeRules.applicableRules goal fun (x : Aesop.Rule Aesop.UnsafeRuleInfo) => !Aesop.BaseRuleSet.isErased rs.toBaseRuleSet x.name

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

Equations

• rs.applicableSafeRules goal = rs.safeRules.applicableRules goal fun (x : Aesop.Rule Aesop.SafeRuleInfo) => !Aesop.BaseRuleSet.isErased rs.toBaseRuleSet x.name

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.