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

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

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.

Equations

• d.mapArraysM f = do let __do_lift ← d.root.mapM fun (t : Lean.Meta.DiscrTree.Trie α) => t.mapArraysM f pure { root := __do_lift }

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