structure Aesop.Index (α : Type) : Type

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

Instances For

• Aesop.Index.instEmptyCollection
• Aesop.instInhabitedIndex

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

Equations

• Aesop.instInhabitedIndex = { default := { byTarget := default, byHyp := default, unindexed := 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.

def Aesop.Index.trace.traceArray {α : Type} [ToString (Rule α)] (traceOpt : TraceOption) (as : Array (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

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

Equations

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

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.

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

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 : 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) (include? : Rule α → Bool) : Lean.MetaM (Array (IndexMatchResult (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 (Rule α) (Array IndexMatchLocation) Rule.compareByPriorityThenName) (rs : Array (Rule α × Array IndexMatchLocation)) : Lean.RBMap (Rule α) (Array IndexMatchLocation) Rule.compareByPriorityThenName

Equations

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