inductive Lean.NamePart : Type

• str: String → Lean.NamePart
• num: Nat → Lean.NamePart

instance Lean.instToStringNamePart : ToString Lean.NamePart

def Lean.NamePart.cmp : Lean.NamePart → Lean.NamePart → Ordering

def Lean.NamePart.lt : Lean.NamePart → Lean.NamePart → Bool

def Lean.NameTrie (β : Type u) : Type u

def Lean.NameTrie.insert {β : Type u_1} (t : Lean.NameTrie β) (n : Lake.Name) (b : β) : Lean.NameTrie β

def Lean.NameTrie.empty {β : Type u_1} : Lean.NameTrie β

instance Lean.instInhabitedNameTrie {β : Type u_1} : Inhabited (Lean.NameTrie β)

instance Lean.instEmptyCollectionNameTrie {β : Type u_1} : EmptyCollection (Lean.NameTrie β)

def Lean.NameTrie.find? {β : Type u_1} (t : Lean.NameTrie β) (k : Lake.Name) : Option β

@[inline]

def Lean.NameTrie.foldMatchingM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} [Monad m] (t : Lean.NameTrie β) (k : Lake.Name) (init : σ) (f : β → σ → m σ) : m σ

@[inline]

def Lean.NameTrie.foldM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} [Monad m] (t : Lean.NameTrie β) (init : σ) (f : β → σ → m σ) : m σ

@[inline]

def Lean.NameTrie.forMatchingM {m : Type → Type u_1} {β : Type u_2} [Monad m] (t : Lean.NameTrie β) (k : Lake.Name) (f : β → m Unit) : m Unit

@[inline]

def Lean.NameTrie.forM {m : Type → Type u_1} {β : Type u_2} [Monad m] (t : Lean.NameTrie β) (f : β → m Unit) : m Unit