inductive Lean.NamePart : Type

• str (s : String) : NamePart
• num (n : Nat) : NamePart

@[implicit_reducible]

instance Lean.instToStringNamePart : ToString NamePart

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

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

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[inline]

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

Returns the value of the longest key in t that is a prefix of k, if any.

@[inline]

def Lean.NameTrie.foldMatchingM {m : Type u_1 → Type u_2} {β : Type u_3} {σ : Type u_1} [Monad m] (t : NameTrie β) (k : 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 : NameTrie β) (init : σ) (f : β → σ → m σ) : m σ

@[inline]

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

@[inline]

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

def Lean.NameTrie.matchingToArray {β : Type u_1} (t : NameTrie β) (k : Name) : Array β

def Lean.NameTrie.toArray {β : Type u_1} (t : NameTrie β) : Array β