structure Aesop.Index (α : Type) [BEq α] [Hashable α] : Type

• byTarget : Lean.Meta.DiscrTree α Aesop.simpleReduce
• byHyp : Lean.Meta.DiscrTree α Aesop.simpleReduce
• unindexed : Lean.PHashSet α

instance Aesop.instInhabitedIndex : {a : Type} → {a_1 : BEq a} → {a_2 : Hashable a} → Inhabited (Aesop.Index a)

Equations

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

def Aesop.Index.trace {α : Type} [BEq α] [Hashable α] [ToString α] (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 α] (traceOpt : Aesop.TraceOption) (as : Array α) : Lean.CoreM Unit

Equations

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

instance Aesop.Index.instEmptyCollectionIndex {α : Type} [BEq α] [Hashable α] : EmptyCollection (Aesop.Index α)

Equations

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

def Aesop.Index.merge {α : Type} [BEq α] [Hashable α] (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} [BEq α] [Hashable α] (r : α) (imode : Aesop.IndexingMode) (ri : Aesop.Index α) : Aesop.Index α

def Aesop.Index.unindex {α : Type} [BEq α] [Hashable α] (ri : Aesop.Index α) (p : α → Bool) : Aesop.Index α

Equations

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

@[always_inline]

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

Equations

• Aesop.Index.unindex.filterDiscrTree' p unindexed t = Aesop.filterDiscrTree (not ∘ p) (fun unindexed v => Lean.PersistentHashSet.insert unindexed v) unindexed t

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

Equations

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

@[inline]

def Aesop.Index.fold {α : Type} [BEq α] [Hashable α] {σ : Type u_1} (ri : Aesop.Index α) (f : σ → α → σ) (init : σ) : σ

Equations

• Aesop.Index.fold ri f init = Id.run (Aesop.Index.foldM ri f init)

def Aesop.Index.size {α : Type} [BEq α] [Hashable α] : Aesop.Index α → Nat

Equations

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

@[specialize #[]]

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

Equations

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

@[inline]

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

Equations

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