Documentation

Std.Lean.Meta.DiscrTree

Compare two Keys. The ordering is total but otherwise arbitrary. (It uses Name.quickCmp internally.)

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • Lean.Meta.DiscrTree.Key.instOrdKey = { compare := Lean.Meta.DiscrTree.Key.cmp }
@[implemented_by _private.Std.Lean.Meta.DiscrTree.0.Lean.Meta.DiscrTree.Trie.foldMUnsafe]
opaque Lean.Meta.DiscrTree.Trie.foldM {m : Type u_1 → Type u_2} {s : Bool} {σ : Type u_1} {α : Type} [inst : Monad m] (initalKeys : Array (Lean.Meta.DiscrTree.Key s)) (f : σArray (Lean.Meta.DiscrTree.Key s)αm σ) (init : σ) (t : Lean.Meta.DiscrTree.Trie α s) :
m σ

Monadically fold the keys and values stored in a Trie.

@[inline]
def Lean.Meta.DiscrTree.Trie.fold {s : Bool} {σ : Type u_1} {α : Type} (initialKeys : Array (Lean.Meta.DiscrTree.Key s)) (f : σArray (Lean.Meta.DiscrTree.Key s)ασ) (init : σ) (t : Lean.Meta.DiscrTree.Trie α s) :
σ

Fold the keys and values stored in a Trie.

Equations
@[implemented_by _private.Std.Lean.Meta.DiscrTree.0.Lean.Meta.DiscrTree.Trie.foldValuesMUnsafe]
opaque Lean.Meta.DiscrTree.Trie.foldValuesM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} {s : Bool} [inst : Monad m] (f : σαm σ) (init : σ) (t : Lean.Meta.DiscrTree.Trie α s) :
m σ

Monadically fold the values stored in a Trie.

@[inline]
def Lean.Meta.DiscrTree.Trie.foldValues {σ : Type u_1} {α : Type} {s : Bool} (f : σασ) (init : σ) (t : Lean.Meta.DiscrTree.Trie α s) :
σ

Fold the values stored in a Trie.

Equations

The number of values stored in a Trie.

Merge two Tries. Duplicate values are preserved.

@[inline]
def Lean.Meta.DiscrTree.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {s : Bool} {α : Type} [inst : Monad m] (f : σArray (Lean.Meta.DiscrTree.Key s)αm σ) (init : σ) (t : Lean.Meta.DiscrTree α s) :
m σ

Monadically fold over the keys and values stored in a DiscrTree.

Equations
@[inline]
def Lean.Meta.DiscrTree.fold {σ : Type u_1} {s : Bool} {α : Type} (f : σArray (Lean.Meta.DiscrTree.Key s)ασ) (init : σ) (t : Lean.Meta.DiscrTree α s) :
σ

Fold over the keys and values stored in a DiscrTree

Equations
@[inline]
def Lean.Meta.DiscrTree.foldValuesM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} {s : Bool} [inst : Monad m] (f : σαm σ) (init : σ) (t : Lean.Meta.DiscrTree α s) :
m σ

Monadically fold over the values stored in a DiscrTree.

Equations
@[inline]
def Lean.Meta.DiscrTree.foldValues {σ : Type u_1} {α : Type} {s : Bool} (f : σασ) (init : σ) (t : Lean.Meta.DiscrTree α s) :
σ

Fold over the values stored in a DiscrTree.

Equations
@[inline]

Extract the values stored in a DiscrTree.

Equations
@[inline]

Extract the keys and values stored in a DiscrTree.

Equations
@[inline]

Get the number of values stored in a DiscrTree. O(n) in the size of the tree.

Equations
@[inline]

Merge two DiscrTrees. Duplicate values are preserved.

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