partial def Lean.Meta.DiscrTree.Trie.foldM {m : Type u_1 → Type u_2} {σ : Type u_1} {α : Type} [Monad m] (initialKeys : Array Key) (f : σ → Array Key → α → m σ) (init : σ) : Trie α → m σ

Monadically fold the keys and values stored in a Trie.

@[inline]

def Lean.Meta.DiscrTree.Trie.fold {σ : Type u_1} {α : Type} (initialKeys : Array Key) (f : σ → Array Key → α → σ) (init : σ) (t : Trie α) : σ

Fold the keys and values stored in a Trie.

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

Monadically fold the values stored in a Trie.

@[inline]

def Lean.Meta.DiscrTree.Trie.foldValues {σ : Type u_1} {α : Type} (f : σ → α → σ) (init : σ) (t : Trie α) : σ

Fold the values stored in a Trie.

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

The number of values stored in a Trie.

@[inline]

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

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

@[inline]

def Lean.Meta.DiscrTree.fold {σ : Type u_1} {α : Type} (f : σ → Array Key → α → σ) (init : σ) (t : DiscrTree α) : σ

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} [Monad m] (f : σ → α → m σ) (init : σ) (t : DiscrTree α) : m σ

Monadically fold over the values stored in a DiscrTree.

@[inline]

def Lean.Meta.DiscrTree.foldValues {σ : Type u_1} {α : Type} (f : σ → α → σ) (init : σ) (t : DiscrTree α) : σ

Fold over the values stored in a DiscrTree.

@[inline]

def Lean.Meta.DiscrTree.containsValueP {α : Type} (t : DiscrTree α) (f : α → Bool) : Bool

Check for the presence of a value satisfying a predicate.

@[inline]

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

Extract the values stored in a DiscrTree.

@[inline]

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

Extract the keys and values stored in a DiscrTree.

@[inline]

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

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

partial def Lean.Meta.DiscrTree.Trie.mapArraysM {m : Type → Type} [Monad m] {α β : Type} (t : Trie α) (f : Array α → m (Array β)) : m (Trie β)

Apply a monadic function to the array of values at each node in a DiscrTree.

def Lean.Meta.DiscrTree.mapArraysM {m : Type → Type} [Monad m] {α β : Type} (d : DiscrTree α) (f : Array α → m (Array β)) : m (DiscrTree β)

Apply a monadic function to the array of values at each node in a DiscrTree.

def Lean.Meta.DiscrTree.mapArrays {α β : Type} (d : DiscrTree α) (f : Array α → Array β) : DiscrTree β

Apply a function to the array of values at each node in a DiscrTree.