def Lean.Meta.DiscrTree.Key.cmp {s : Bool} : Lean.Meta.DiscrTree.Key s → Lean.Meta.DiscrTree.Key s → Ordering

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

instance Lean.Meta.DiscrTree.Key.instOrdKey {s : Bool} : Ord (Lean.Meta.DiscrTree.Key s)

@[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} [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.

@[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} [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.

partial def Lean.Meta.DiscrTree.Trie.size {α : Type} {s : Bool} : Lean.Meta.DiscrTree.Trie α s → Nat

The number of values stored in a Trie.

partial def Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates {α : Type} {s : Bool} : Lean.Meta.DiscrTree.Trie α s → Lean.Meta.DiscrTree.Trie α s → Lean.Meta.DiscrTree.Trie α s

Merge two Tries. Duplicate values are preserved.

partial def Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates.mergeChildren {α : Type} {s : Bool} (cs₁ : Array (Lean.Meta.DiscrTree.Key s × Lean.Meta.DiscrTree.Trie α s)) (cs₂ : Array (Lean.Meta.DiscrTree.Key s × Lean.Meta.DiscrTree.Trie α s)) : Array (Lean.Meta.DiscrTree.Key s × Lean.Meta.DiscrTree.Trie α s)

Auxiliary definition for mergePreservingDuplicates.

@[inline]

def Lean.Meta.DiscrTree.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {s : Bool} {α : Type} [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.

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

@[inline]

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

Monadically fold over the values stored in a DiscrTree.

@[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.

@[inline]

def Lean.Meta.DiscrTree.values {α : Type} {s : Bool} (t : Lean.Meta.DiscrTree α s) : Array α

Extract the values stored in a DiscrTree.

@[inline]

def Lean.Meta.DiscrTree.toArray {α : Type} {s : Bool} (t : Lean.Meta.DiscrTree α s) : Array (Array (Lean.Meta.DiscrTree.Key s) × α)

Extract the keys and values stored in a DiscrTree.

@[inline]

def Lean.Meta.DiscrTree.size {α : Type} {s : Bool} (t : Lean.Meta.DiscrTree α s) : Nat

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

@[inline]

def Lean.Meta.DiscrTree.mergePreservingDuplicates {α : Type} {s : Bool} (t : Lean.Meta.DiscrTree α s) (u : Lean.Meta.DiscrTree α s) : Lean.Meta.DiscrTree α s

Merge two DiscrTrees. Duplicate values are preserved.