inductive Aesop.RuleSetMember : Type

• normRule: Aesop.NormRule → Aesop.RuleSetMember
• unsafeRule: Aesop.UnsafeRule → Aesop.RuleSetMember
• safeRule: Aesop.SafeRule → Aesop.RuleSetMember
• normSimpRule: Aesop.NormSimpRule → Aesop.RuleSetMember
• localNormSimpRule: Aesop.LocalNormSimpRule → Aesop.RuleSetMember
• unfoldRule: Aesop.UnfoldRule → Aesop.RuleSetMember

instance Aesop.instInhabitedRuleSetMember : Inhabited Aesop.RuleSetMember

Equations

• Aesop.instInhabitedRuleSetMember = { default := Aesop.RuleSetMember.normRule default }

def Aesop.RuleSetMember.name : Aesop.RuleSetMember → Aesop.RuleName

Equations

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

def Aesop.RuleSetMember.isGlobal (m : Aesop.RuleSetMember) : Bool

Equations

• Aesop.RuleSetMember.isGlobal m = ((Aesop.RuleSetMember.name m).scope == Aesop.ScopeName.global)

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.match (f : Aesop.RuleNameFilter) (n : Aesop.RuleName) : Bool

Equations

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

structure Aesop.RuleSet : Type

• normRules : Aesop.Index Aesop.NormRule
• unsafeRules : Aesop.Index Aesop.UnsafeRule
• safeRules : Aesop.Index Aesop.SafeRule
• normSimpLemmas : Lean.Meta.SimpTheorems
• normSimpLemmaDescrs : Lean.PHashMap Aesop.RuleName (Array Lean.Meta.SimpEntry)
• localNormSimpLemmas : Array Aesop.LocalNormSimpRule
• unfoldRules : Lean.PHashMap Lean.Name (Option Lean.Name)
• ruleNames : Lean.PHashMap Aesop.RuleIdent (Aesop.UnorderedArraySet Aesop.RuleName)
• erased : Lean.HashSet Aesop.RuleName

instance Aesop.instInhabitedRuleSet : Inhabited Aesop.RuleSet

Equations

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

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

Equations

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

def Aesop.RuleSet.empty : Aesop.RuleSet

Equations

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

instance Aesop.RuleSet.instEmptyCollectionRuleSet : EmptyCollection Aesop.RuleSet

Equations

• Aesop.RuleSet.instEmptyCollectionRuleSet = { emptyCollection := Aesop.RuleSet.empty }

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

Equations

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

def Aesop.RuleSet.add (rs : Aesop.RuleSet) (r : Aesop.RuleSetMember) : Aesop.RuleSet

Equations

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

def Aesop.RuleSet.addArray (rs : Aesop.RuleSet) (ra : Array Aesop.RuleSetMember) : Aesop.RuleSet

Equations

• Aesop.RuleSet.addArray rs ra = Array.foldl Aesop.RuleSet.add rs ra 0 (Array.size ra)

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

Equations

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

def Aesop.RuleSet.eraseAllRulesWithIdent (rs : Aesop.RuleSet) (i : Aesop.RuleIdent) : Aesop.RuleSet × Bool

Equations

• Aesop.RuleSet.eraseAllRulesWithIdent rs i = Aesop.RuleSet.erase rs (Aesop.RuleNameFilter.ofIdent i)

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

Equations

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

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

Equations

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

def Aesop.RuleSet.rulesMatching (rs : Aesop.RuleSet) (f : Aesop.RuleNameFilter) : Aesop.UnorderedArraySet Aesop.RuleName

Equations

• Aesop.RuleSet.rulesMatching rs f = match Lean.PersistentHashMap.find? rs.ruleNames f.ident with | none => ∅ | some ns => Aesop.UnorderedArraySet.filter (Aesop.RuleNameFilter.match f) ns

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

Equations

• Aesop.RuleSet.applicableNormalizationRules rs goal = Aesop.Index.applicableRules rs.normRules goal fun x => !Aesop.RuleSet.isErased rs x.name

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

Equations

• Aesop.RuleSet.applicableUnsafeRules rs goal = Aesop.Index.applicableRules rs.unsafeRules goal fun x => !Aesop.RuleSet.isErased rs x.name

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

Equations

• Aesop.RuleSet.applicableSafeRules rs goal = Aesop.Index.applicableRules rs.safeRules goal fun x => !Aesop.RuleSet.isErased rs x.name

def Aesop.RuleSet.foldM {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (rs : Aesop.RuleSet) (f : σ → Aesop.RuleSetMember → m σ) (init : σ) : m σ

Equations

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

@[inline]

def Aesop.RuleSet.foldM.go {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (rs : Aesop.RuleSet) (f : σ → Aesop.RuleSetMember → m σ) (s : σ) (r : Aesop.RuleSetMember) : m σ

Equations

• Aesop.RuleSet.foldM.go rs f s r = if Aesop.RuleSet.isErased rs (Aesop.RuleSetMember.name r) = true then pure s else f s r

@[inline]

def Aesop.RuleSet.fold {σ : Type u_1} (rs : Aesop.RuleSet) (f : σ → Aesop.RuleSetMember → σ) (init : σ) : σ

Equations

• Aesop.RuleSet.fold rs f init = Id.run (Aesop.RuleSet.foldM rs f init)

@[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, Aesop.localRuleSetName]

def Aesop.defaultEnabledRuleSetNames : Array Aesop.RuleSetName

Equations

• Aesop.defaultEnabledRuleSetNames = Aesop.builtinRuleSetNames

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

Equations

• Aesop.RuleSetName.isReserved n = 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.match (f : Aesop.RuleSetNameFilter) (n : Aesop.RuleSetName) : Bool

Equations

• Aesop.RuleSetNameFilter.match 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.RuleSets : Type

• rs : Lean.HashMap Aesop.RuleSetName Aesop.RuleSet

instance Aesop.instInhabitedRuleSets : Inhabited Aesop.RuleSets

Equations

• Aesop.instInhabitedRuleSets = { default := { rs := default } }

def Aesop.RuleSets.empty : Aesop.RuleSets

Equations

• Aesop.RuleSets.empty = { rs := ∅ }

instance Aesop.RuleSets.instEmptyCollectionRuleSets : EmptyCollection Aesop.RuleSets

Equations

• Aesop.RuleSets.instEmptyCollectionRuleSets = { emptyCollection := Aesop.RuleSets.empty }

def Aesop.RuleSets.trace (rss : Aesop.RuleSets) (opt : Aesop.TraceOption) : Lean.CoreM Unit

Equations

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

def Aesop.RuleSets.trace.compareRuleSets (x : Aesop.RuleSetName × Aesop.RuleSet) (y : Aesop.RuleSetName × Aesop.RuleSet) : Bool

Equations

• Aesop.RuleSets.trace.compareRuleSets x y = Ordering.isLT (Lean.Name.cmp x.fst y.fst)

def Aesop.RuleSets.addEmptyRuleSet (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) : Aesop.RuleSets

Equations

• Aesop.RuleSets.addEmptyRuleSet rss rsName = { rs := Lean.HashMap.insert rss.rs rsName ∅ }

def Aesop.RuleSets.addRuleSet (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) (rs : Aesop.RuleSet) : Aesop.RuleSets

Equations

• Aesop.RuleSets.addRuleSet rss rsName rs = { rs := Lean.HashMap.insert rss.rs rsName rs }

def Aesop.RuleSets.containsRuleSet (rss : Aesop.RuleSets) (name : Aesop.RuleSetName) : Bool

Equations

• Aesop.RuleSets.containsRuleSet rss name = Lean.HashMap.contains rss.rs name

def Aesop.RuleSets.ensureRuleSet (rss : Aesop.RuleSets) (name : Aesop.RuleSetName) : Aesop.RuleSets

Equations

• Aesop.RuleSets.ensureRuleSet rss name = if Aesop.RuleSets.containsRuleSet rss name = true then rss else Aesop.RuleSets.addEmptyRuleSet rss name

def Aesop.RuleSets.eraseRuleSet (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) : Aesop.RuleSets

Equations

• Aesop.RuleSets.eraseRuleSet rss rsName = { rs := Lean.HashMap.erase rss.rs rsName }

def Aesop.RuleSets.getRuleSet? (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) : Option Aesop.RuleSet

Equations

• Aesop.RuleSets.getRuleSet? rss rsName = Lean.HashMap.find? rss.rs rsName

@[inline]

def Aesop.RuleSets.modifyRuleSetM {m : Type → Type u_1} [Monad m] (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) (f : Aesop.RuleSet → m Aesop.RuleSet) : m Aesop.RuleSets

Equations

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

@[inline]

def Aesop.RuleSets.modifyRuleSet (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) (f : Aesop.RuleSet → Aesop.RuleSet) : Aesop.RuleSets

Equations

• Aesop.RuleSets.modifyRuleSet rss rsName f = Id.run (Aesop.RuleSets.modifyRuleSetM rss rsName fun rs => pure (f rs))

def Aesop.RuleSets.containsRule (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) (rName : Aesop.RuleName) : Bool

Equations

• Aesop.RuleSets.containsRule rss rsName rName = match Aesop.RuleSets.getRuleSet? rss rsName with | none => false | some rs => Aesop.RuleSet.contains rs rName

def Aesop.RuleSets.addRuleUnchecked (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) (r : Aesop.RuleSetMember) : Aesop.RuleSets

Equations

• Aesop.RuleSets.addRuleUnchecked rss rsName r = Aesop.RuleSets.modifyRuleSet rss rsName fun x => Aesop.RuleSet.add x r

def Aesop.RuleSets.addRuleChecked {m : Type → Type} [Monad m] [Lean.MonadError m] (rss : Aesop.RuleSets) (rsName : Aesop.RuleSetName) (rule : Aesop.RuleSetMember) : m Aesop.RuleSets

Equations

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

def Aesop.RuleSets.eraseRules (rss : Aesop.RuleSets) (rsf : Aesop.RuleSetNameFilter) (rf : Aesop.RuleNameFilter) : Aesop.RuleSets × Bool

Equations

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

def Aesop.RuleSets.eraseRulesChecked {m : Type → Type} [Monad m] [Lean.MonadError m] (rss : Aesop.RuleSets) (rsf : Aesop.RuleSetNameFilter) (rf : Aesop.RuleNameFilter) : m Aesop.RuleSets

Equations

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

@[always_inline]

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

Equations

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

def Aesop.RuleSets.getMergedRuleSet (rss : Aesop.RuleSets) (options : Aesop.Options) : Aesop.RuleSet

Equations

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