Documentation

Lean.Data.NameTrie

inductive Lean.NamePart :

Type

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

instance Lean.instToStringNamePart :

ToString Lean.NamePart

Equations

Lean.instToStringNamePart = { toString := fun x => match x with | Lean.NamePart.str s => s | Lean.NamePart.num n => toString n }

def Lean.NamePart.cmp :

Lean.NamePart → Lean.NamePart → Ordering

Equations

Lean.NamePart.cmp x x = match x, x with | Lean.NamePart.str a, Lean.NamePart.str b => compare a b | Lean.NamePart.num a, Lean.NamePart.num b => compare a b | Lean.NamePart.num x, Lean.NamePart.str x_1 => Ordering.lt | x, x_1 => Ordering.gt

def Lean.NamePart.lt :

Lean.NamePart → Lean.NamePart → Bool

Equations

Lean.NamePart.lt x x = match x, x with | Lean.NamePart.str a, Lean.NamePart.str b => decide (a < b) | Lean.NamePart.num a, Lean.NamePart.num b => decide (a < b) | Lean.NamePart.num x, Lean.NamePart.str x_1 => true | x, x_1 => false

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

Type u

Equations

Lean.NameTrie β = Lean.PrefixTree Lean.NamePart β Lean.NamePart.cmp

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

Lean.NameTrie β

Equations

Lean.NameTrie.insert t n b = Lean.PrefixTree.insert t (Lean.toKey n) b

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

Lean.NameTrie β

Equations

Lean.NameTrie.empty = Lean.PrefixTree.empty

instance Lean.instInhabitedNameTrie {β : Type u_1} :

Inhabited (Lean.NameTrie β)

Equations

Lean.instInhabitedNameTrie = { default := Lean.NameTrie.empty }

instance Lean.instEmptyCollectionNameTrie {β : Type u_1} :

EmptyCollection (Lean.NameTrie β)

Equations

Lean.instEmptyCollectionNameTrie = { emptyCollection := Lean.NameTrie.empty }

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

Equations

Lean.NameTrie.find? t k = Lean.PrefixTree.find? t (Lean.toKey k)

@[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

Lean.NameTrie.foldMatchingM t k init f = Lean.PrefixTree.foldMatchingM t (Lean.toKey k) init f

@[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

Lean.NameTrie.foldM t init f = Lean.NameTrie.foldMatchingM t Lean.Name.anonymous init f

@[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) :

Equations

Lean.NameTrie.forMatchingM t k f = Lean.PrefixTree.forMatchingM t (Lean.toKey k) f

@[inline]

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

Equations

Lean.NameTrie.forM t f = Lean.NameTrie.forMatchingM t Lean.Name.anonymous f