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

Equations

• Lean.Meta.DiscrTree.Trie.fold initialKeys f init t = (Lean.Meta.DiscrTree.Trie.foldM initialKeys (fun (s : σ) (k : Array Lean.Meta.DiscrTree.Key) (a : α) => pure (f s k a)) init t).run

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

Equations

• Lean.Meta.DiscrTree.Trie.foldValues f init t = (Lean.Meta.DiscrTree.Trie.foldValuesM (fun (x1 : σ) (x2 : α) => pure (f x1 x2)) init t).run

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.

Equations

• Lean.Meta.DiscrTree.Trie.mkNode vs cs = Lean.Meta.DiscrTree.Trie.node vs cs

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

Equations

• (Lean.Meta.DiscrTree.Trie.node vs children).asNode = (vs, 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.

Equations

• (Lean.Meta.DiscrTree.Trie.node vs children).nodeValues = vs

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

Equations

• (Lean.Meta.DiscrTree.Trie.node vs children).nodeChildren = children

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

Equations

• (Lean.Meta.DiscrTree.Trie.node vs children).isEmptyNode = (vs.isEmpty && children.isEmpty)

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

Equations

• Lean.Meta.DiscrTree.foldM f init t = t.root.foldlM (fun (s : σ) (k : Lean.Meta.DiscrTree.Key) (t : Lean.Meta.DiscrTree.Trie α) => Lean.Meta.DiscrTree.Trie.foldM #[k] f s t) init

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

Equations

• Lean.Meta.DiscrTree.fold f init t = (Lean.Meta.DiscrTree.foldM (fun (s : σ) (keys : Array Lean.Meta.DiscrTree.Key) (a : α) => pure (f s keys a)) init t).run

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

Equations

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

@[inline]

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

Fold over the values stored in a DiscrTree.

Equations

• Lean.Meta.DiscrTree.foldValues f init t = (Lean.Meta.DiscrTree.foldValuesM (fun (x1 : σ) (x2 : α) => pure (f x1 x2)) init t).run

@[inline]

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

Check for the presence of a value satisfying a predicate.

Equations

• t.containsValueP f = Lean.Meta.DiscrTree.foldValues (fun (r : Bool) (a : α) => r || f a) false t

@[inline]

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

Extract the values stored in a DiscrTree.

Equations

• t.values = Lean.Meta.DiscrTree.foldValues (fun (as : Array α) (a : α) => as.push a) #[] t

@[inline]

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

Extract the keys and values stored in a DiscrTree.

Equations

• t.toArray = Lean.Meta.DiscrTree.fold (fun (as : Array (Array Lean.Meta.DiscrTree.Key × α)) (keys : Array Lean.Meta.DiscrTree.Key) (a : α) => as.push (keys, a)) #[] t

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

Equations

• t.size = t.root.foldl (fun (n : Nat) (x : Lean.Meta.DiscrTree.Key) (t : Lean.Meta.DiscrTree.Trie α) => n + t.size) 0

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

Equations

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

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

Equations

• d.mapArrays f = (d.mapArraysM fun (A : Array α) => pure (f A)).run