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 : Index NormRuleInfo

  Normalisation rules registered in this rule set.

• unsafeRules : Index UnsafeRuleInfo

  Unsafe rules registered in this rule set.

• safeRules : Index 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.

• forwardRules : ForwardIndex

  Forward rules. There's a special procedure for applying forward rules, so we don't store them in the regular indices.

• forwardRuleNames : Lean.PHashSet RuleName

  The names of all rules in forwardRules.

• rulePatterns : RulePatternIndex

  An index for the rule patterns associated with rules contained in this rule set. When rules are removed from the rule set, their patterns are not removed from this index.

• erased : Lean.PHashSet RuleName

  The set of rules that were erased from normRules, unsafeRules, safeRules and forwardRules. When we erase a rule which is present in any of these four 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 (UnorderedArraySet 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, forwardRules 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 BaseRuleSet

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 : Index NormRuleInfo
• unsafeRules : Index UnsafeRuleInfo
• safeRules : Index SafeRuleInfo
• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)
• forwardRules : ForwardIndex
• forwardRuleNames : Lean.PHashSet RuleName
• rulePatterns : RulePatternIndex
• erased : Lean.PHashSet RuleName
• ruleNames : Lean.PHashMap Lean.Name (UnorderedArraySet 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 GlobalRuleSet

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 : Index NormRuleInfo
• unsafeRules : Index UnsafeRuleInfo
• safeRules : Index SafeRuleInfo
• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)
• forwardRules : ForwardIndex
• forwardRuleNames : Lean.PHashSet RuleName
• rulePatterns : RulePatternIndex
• erased : Lean.PHashSet RuleName
• ruleNames : Lean.PHashMap Lean.Name (UnorderedArraySet 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 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 : BaseRuleSet → m (BaseRuleSet × α)) (rs : GlobalRuleSet) : m (GlobalRuleSet × α)

@[always_inline]

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

@[always_inline]

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

@[always_inline]

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

@[always_inline]

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

@[always_inline]

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

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

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

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

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

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

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

def Aesop.BaseRuleSet.empty : BaseRuleSet

instance Aesop.instEmptyCollectionBaseRuleSet : EmptyCollection BaseRuleSet

def Aesop.GlobalRuleSet.empty : GlobalRuleSet

instance Aesop.instEmptyCollectionGlobalRuleSet : EmptyCollection GlobalRuleSet

def Aesop.LocalRuleSet.empty : LocalRuleSet

instance Aesop.instEmptyCollectionLocalRuleSet : EmptyCollection LocalRuleSet

instance Aesop.instInhabitedLocalRuleSet : Inhabited LocalRuleSet

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

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

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

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

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

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

def Aesop.BaseRuleSet.add.addRulePattern (n : RuleName) (pat? : Option RulePattern) (rs : BaseRuleSet) : BaseRuleSet

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

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

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

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

def Aesop.LocalRuleSet.applicableNormalizationRulesWith (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) (include? : NormRule → Bool) : BaseM (Array (IndexMatchResult NormRule))

@[always_inline]

def Aesop.LocalRuleSet.applicableNormalizationRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) : BaseM (Array (IndexMatchResult NormRule))

def Aesop.LocalRuleSet.applicableUnsafeRulesWith (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) (include? : UnsafeRule → Bool) : BaseM (Array (IndexMatchResult UnsafeRule))

@[always_inline]

def Aesop.LocalRuleSet.applicableUnsafeRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) : BaseM (Array (IndexMatchResult UnsafeRule))

def Aesop.LocalRuleSet.applicableSafeRulesWith (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) (include? : SafeRule → Bool) : BaseM (Array (IndexMatchResult SafeRule))

@[always_inline]

def Aesop.LocalRuleSet.applicableSafeRules (rs : LocalRuleSet) (fms : ForwardRuleMatches) (goal : Lean.MVarId) : BaseM (Array (IndexMatchResult SafeRule))

def Aesop.LocalRuleSet.applicableForwardRulesWith (rs : LocalRuleSet) (e : Lean.Expr) (include? : ForwardRule → Bool) : Lean.MetaM (Array (ForwardRule × PremiseIndex))

def Aesop.LocalRuleSet.applicableForwardRulesWith.mkMsg (r : ForwardRule) (i : PremiseIndex) : Lean.MessageData

@[always_inline]

def Aesop.LocalRuleSet.applicableForwardRules (rs : LocalRuleSet) (e : Lean.Expr) : Lean.MetaM (Array (ForwardRule × PremiseIndex))

def Aesop.LocalRuleSet.constForwardRuleMatches (rs : LocalRuleSet) : Array ForwardRuleMatch

def Aesop.LocalRuleSet.forwardRulePatternSubstsInExpr (rs : LocalRuleSet) (e : Lean.Expr) : BaseM (Array (ForwardRule × Substitution))

def Aesop.LocalRuleSet.forwardRulePatternSubstsInLocalDecl (rs : LocalRuleSet) (ldecl : Lean.LocalDecl) : BaseM (Array (ForwardRule × Substitution))

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

@[always_inline]

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

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