Documentation

Aesop.Index

Equations
  • Aesop.instInhabitedIndex = { default := { byTarget := default, byHyp := default, unindexed := default } }
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
  • One or more equations did not get rendered due to their size.
def Aesop.Index.merge {α : Type} (ri₁ ri₂ : 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 α) :
def Aesop.Index.unindex {α : Type} (ri : Aesop.Index α) (p : Aesop.Rule αBool) :
Equations
  • One or more equations did not get rendered due to their size.
@[always_inline]
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
@[specialize #[]]
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.