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.
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}
[inst : 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}
[inst : 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)
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))
:
Auxiliary definition for mergePreservingDuplicates.
@[inline]
def
Lean.Meta.DiscrTree.foldM
{m : Type u_1 → Type u_2}
{σ : Type u_1}
{s : Bool}
{α : Type}
[inst : 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}
[inst : 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]
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]
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)
:
Merge two DiscrTrees. Duplicate values are preserved.
Equations
- One or more equations did not get rendered due to their size.