Documentation

Lean.Data.NameTrie

source
inductive Lean.NamePart:
Type
source
instance Lean.instToStringNamePart:
ToString Lean.NamePart
Equations
source
def Lean.NamePart.cmp:
Lean.NamePart → Lean.NamePart → Ordering
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.NamePart.lt:
Lean.NamePart → Lean.NamePart → Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.NameTrie (β : Type u) :
Type u
Equations
source
def Lean.NameTrie.insert {β : Type u_1} (t : Lean.NameTrie β) (n : Lean.Name) (b : β) :
Lean.NameTrie β
Equations
source
def Lean.NameTrie.empty {β : Type u_1} :
Lean.NameTrie β
Equations
  • Lean.NameTrie.empty = Lean.PrefixTree.empty
source
instance Lean.instInhabitedNameTrie {β : Type u_1} :
Inhabited (Lean.NameTrie β)
Equations
  • Lean.instInhabitedNameTrie = { default := Lean.NameTrie.empty }
source
instance Lean.instEmptyCollectionNameTrie {β : Type u_1} :
EmptyCollection (Lean.NameTrie β)
Equations
  • Lean.instEmptyCollectionNameTrie = { emptyCollection := Lean.NameTrie.empty }
source
def Lean.NameTrie.find? {β : Type u_1} (t : Lean.NameTrie β) (k : Lean.Name) :
Option β
Equations
source
@[inline]
def Lean.NameTrie.foldMatchingM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} [inst : Monad m] (t : Lean.NameTrie β) (k : Lean.Name) (init : σ) (f : β → σ → m σ) :
m σ
Equations
source
@[inline]
def Lean.NameTrie.foldM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} [inst : Monad m] (t : Lean.NameTrie β) (init : σ) (f : β → σ → m σ) :
m σ
Equations
source
@[inline]
def Lean.NameTrie.forMatchingM {m : Type → Type u_1} {β : Type u_2} [inst : Monad m] (t : Lean.NameTrie β) (k : Lean.Name) (f : β → m Unit) :
m Unit
Equations
source
@[inline]
def Lean.NameTrie.forM {m : Type → Type u_1} {β : Type u_2} [inst : Monad m] (t : Lean.NameTrie β) (f : β → m Unit) :
m Unit
Equations