structure Aesop.Index (α : Type) : Type

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

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

Equations

• Aesop.instInhabitedIndex = { default := { byTarget := default, byHyp := default, unindexed := default } }

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

Equations

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

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

Equations

• Aesop.Index.trace.traceArray traceOpt as = Array.forM (fun (r : String) => Lean.addTrace traceOpt.traceClass (Lean.toMessageData r)) (Array.map toString as).qsortOrd 0

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

Equations

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

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

Equations

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

@[specialize #[]]

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

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

Equations

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

@[always_inline]

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

Equations

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

def Aesop.Index.foldM {α : Type} {m : Type u_1 → Type u_1} {σ : Type u_1} [Monad m] (ri : Aesop.Index α) (f : σ → Aesop.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 : Aesop.Index α) (f : σ → Aesop.Rule α → σ) (init : σ) : σ

Equations

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

def Aesop.Index.size {α : Type} : Aesop.Index α → Nat

Equations

• x.size = match x with | { byTarget := byTarget, byHyp := byHyp, unindexed := unindexed } => byHyp.size + byTarget.size + Lean.PersistentHashSet.size unindexed

@[specialize #[]]

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

Equations

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

@[inline]

def Aesop.Index.applicableRules.insertIndexMatchResults {α : Type} [Ord α] (m : Lean.RBMap (Aesop.Rule α) (Array Aesop.IndexMatchLocation) Aesop.Rule.compareByPriorityThenName) (rs : Array (Aesop.Rule α × Array Aesop.IndexMatchLocation)) : Lean.RBMap (Aesop.Rule α) (Array Aesop.IndexMatchLocation) Aesop.Rule.compareByPriorityThenName

Equations

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