@[specialize #[]]

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.

@[specialize #[]]

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.Trie.mkNode {α : Type} (vs : Array α) (cs : Array (Key × Trie α)) : Trie α

Generate a trie node from values and an array of children.

@[inline]

def Lean.Meta.DiscrTree.Trie.asNode {α : Type} : Trie α → Array α × Array (Key × Trie α)

Inspect a trie node as an array of values and an array of children.

@[inline]

def Lean.Meta.DiscrTree.Trie.nodeValues {α : Type} : Trie α → Array α

Returns the values stored at the current trie node. Equivalent to t.asNode.1.

@[inline]

def Lean.Meta.DiscrTree.Trie.nodeChildren {α : Type} : Trie α → Array (Key × Trie α)

Returns the child nodes of the current trie node. Equivalent to t.asNode.2.

@[inline]

def Lean.Meta.DiscrTree.Trie.isEmptyNode {α : Type} : Trie α → Bool

Checks whether a trie node is empty (no values and no children).

This is only a check for actual trie emptiness (t.size = 0) if all operations maintain the invariant that no trie node has an empty child node.

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

@[specialize #[]]

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. Any resulting subtrees containing no values will be pruned.

@[inline]

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.

@[inline]

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.