structure Aesop.Index (α : Type) : Type

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

@[implicit_reducible]

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

Equations

• Aesop.instInhabitedIndex = { default := Aesop.instInhabitedIndex.default }

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

Equations

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

@[implicit_reducible]

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

Equations

• Aesop.Index.instEmptyCollection = { emptyCollection := { byTarget := { }, byHyp := { }, unindexed := ∅ } }

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

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Equations

• ri.fold f init = (ri.foldM f init).run

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

Equations

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