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

Equations

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

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

Equations

• Lean.Meta.DiscrTree.Key.instOrdKey = { compare := Lean.Meta.DiscrTree.Key.cmp }

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

Equations

• Lean.Meta.DiscrTree.Trie.fold initialKeys f init t = Id.run (Lean.Meta.DiscrTree.Trie.foldM initialKeys (fun s k a => pure (f s k a)) init t)

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

Equations

• Lean.Meta.DiscrTree.Trie.foldValues f init t = Id.run (Lean.Meta.DiscrTree.Trie.foldValuesM f init t)

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.

Equations

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

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

Equations

• Lean.Meta.DiscrTree.fold f init t = Id.run (Lean.Meta.DiscrTree.foldM (fun s keys a => pure (f s keys a)) init t)

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

Equations

• Lean.Meta.DiscrTree.foldValuesM f init t = Lean.PersistentHashMap.foldlM t.root (fun s x t => Lean.Meta.DiscrTree.Trie.foldValuesM f s t) init

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

Equations

• Lean.Meta.DiscrTree.foldValues f init t = Id.run (Lean.Meta.DiscrTree.foldValuesM f init t)

@[inline]

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

Extract the values stored in a DiscrTree.

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.DiscrTree.size t = Lean.PersistentHashMap.foldl t.root (fun n x t => n + Lean.Meta.DiscrTree.Trie.size t) 0

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

Equations

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