structure Aesop.Index (α : Type) : Type

• byTarget : Lean.Meta.DiscrTree (Rule α)
• byHyp : Lean.Meta.DiscrTree (Rule α)
• unindexed : Lean.PHashSet (Rule α)

instance Aesop.instInhabitedIndex {a✝ : Type} : Inhabited (Index a✝)

def Aesop.Index.trace {α : Type} [ToString (Rule α)] (ri : Index α) (traceOpt : TraceOption) : Lean.CoreM Unit

def Aesop.Index.trace.traceArray {α : Type} [ToString (Rule α)] (traceOpt : TraceOption) (as : Array (Rule α)) : Lean.CoreM Unit

instance Aesop.Index.instEmptyCollection {α : Type} : EmptyCollection (Index α)

def Aesop.Index.merge {α : Type} (ri₁ ri₂ : Index α) : Index α

@[specialize #[]]

partial def Aesop.Index.add {α : Type} (r : Rule α) (imode : IndexingMode) (ri : Index α) : Index α

def Aesop.Index.unindex {α : Type} (ri : Index α) (p : Rule α → Bool) : Index α

@[always_inline]

def Aesop.Index.unindex.filterDiscrTree' {α : Type} (p : Rule α → Bool) (unindexed : Lean.PHashSet (Rule α)) (t : Lean.Meta.DiscrTree (Rule α)) : Lean.Meta.DiscrTree (Rule α) × Lean.PHashSet (Rule α)

def Aesop.Index.foldM {α : Type} {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (ri : Index α) (f : σ → Rule α → m σ) (init : σ) : m σ

@[inline]

def Aesop.Index.fold {α : Type} {σ : Type u_1} (ri : Index α) (f : σ → Rule α → σ) (init : σ) : σ

@[specialize #[]]

def Aesop.Index.applicableRules {α : Type} [Ord α] (ri : Index α) (goal : Lean.MVarId) (patSubstMap : RulePatternSubstMap) (additionalRules : Array (IndexMatchResult (Rule α))) (include? : Rule α → Bool) : Lean.MetaM (Array (IndexMatchResult (Rule α)))

def Aesop.Index.applicableRules.addRules {α : Type} (patSubstMap : RulePatternSubstMap) (acc : Array (IndexMatchResult (Rule α))) (ruless : Array (Array (Rule α × Array IndexMatchLocation))) : Array (IndexMatchResult (Rule α))