def Lean.Meta.DiscrTree.Key.cmp : Lean.Meta.DiscrTree.Key → Lean.Meta.DiscrTree.Key → 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 : Ord Lean.Meta.DiscrTree.Key

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} {σ : Type u_1} {α : Type} [Monad m] (initalKeys : Array Lean.Meta.DiscrTree.Key) (f : σ → Array Lean.Meta.DiscrTree.Key → α → m σ) (init : σ) (t : Lean.Meta.DiscrTree.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 Lean.Meta.DiscrTree.Key) (f : σ → Array Lean.Meta.DiscrTree.Key → α → σ) (init : σ) (t : Lean.Meta.DiscrTree.Trie α) : σ

Fold the keys and values stored in a Trie.

Equations

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

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

Monadically fold the values stored in a Trie.

@[inline]

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

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} : Lean.Meta.DiscrTree.Trie α → Nat

The number of values stored in a Trie.

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

Merge two Tries. Duplicate values are preserved.

partial def Lean.Meta.DiscrTree.Trie.mergePreservingDuplicates.mergeChildren {α : Type} (cs₁ : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) (cs₂ : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)) : Array (Lean.Meta.DiscrTree.Key × Lean.Meta.DiscrTree.Trie α)

Auxiliary definition for mergePreservingDuplicates.

@[inline]

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

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

Equations

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

@[inline]

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

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

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} (t : Lean.Meta.DiscrTree α) : Array α

Extract the values stored in a DiscrTree.

Equations

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

@[inline]

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

Extract the keys and values stored in a DiscrTree.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

def Lean.Meta.DiscrTree.mergePreservingDuplicates {α : Type} (t : Lean.Meta.DiscrTree α) (u : Lean.Meta.DiscrTree α) : Lean.Meta.DiscrTree α

Merge two DiscrTrees. Duplicate values are preserved.

Equations

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

def Lean.Meta.DiscrTree.insertIfSpecific {α : Type} [BEq α] (d : Lean.Meta.DiscrTree α) (keys : Array Lean.Meta.DiscrTree.Key) (v : α) (config : Lean.Meta.WhnfCoreConfig) : Lean.Meta.DiscrTree α

Inserts a new key into a discrimination tree, but only if it is not of the form #[*] or #[=, *, *, *].

Equations

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

partial def Lean.Meta.DiscrTree.Trie.mapArraysM {m : Type → Type} [Monad m] {α : Type} {β : Type} (t : Lean.Meta.DiscrTree.Trie α) (f : Array α → m (Array β)) : m (Lean.Meta.DiscrTree.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} {β : Type} (d : Lean.Meta.DiscrTree α) (f : Array α → m (Array β)) : m (Lean.Meta.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.

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

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

Equations

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