inductive Lean.NamePart : Type

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

@[instance_reducible]

instance Lean.instBEqNamePart : BEq NamePart

Equations

• Lean.instBEqNamePart = { beq := Lean.instBEqNamePart.beq }

def Lean.instBEqNamePart.beq : NamePart → NamePart → Bool

Equations

• Lean.instBEqNamePart.beq (Lean.NamePart.str a) (Lean.NamePart.str b) = (a == b)
• Lean.instBEqNamePart.beq (Lean.NamePart.num a) (Lean.NamePart.num b) = (a == b)
• Lean.instBEqNamePart.beq x✝¹ x✝ = false

@[instance_reducible]

instance Lean.instInhabitedNamePart : Inhabited NamePart

Equations

• Lean.instInhabitedNamePart = { default := Lean.instInhabitedNamePart.default }

@[instance_reducible]

instance Lean.instToStringNamePart : ToString NamePart

Equations

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

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

Equations

• (Lean.NamePart.str a).cmp (Lean.NamePart.str b) = compare a b
• (Lean.NamePart.num a).cmp (Lean.NamePart.num b) = compare a b
• (Lean.NamePart.num n).cmp (Lean.NamePart.str s) = Ordering.lt
• x✝¹.cmp x✝ = Ordering.gt

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

Equations

• (Lean.NamePart.str a).lt (Lean.NamePart.str b) = decide (a < b)
• (Lean.NamePart.num a).lt (Lean.NamePart.num b) = decide (a < b)
• (Lean.NamePart.num n).lt (Lean.NamePart.str s) = true
• x✝¹.lt x✝ = false

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 : NameTrie β) (n : Name) (b : β) : NameTrie β

Equations

• t.insert n b = Lean.PrefixTree.insert t (Lean.toKey✝ n) b

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

Equations

• Lean.NameTrie.empty = Lean.PrefixTree.empty

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

• t.find? k = Lean.PrefixTree.find? t (Lean.toKey✝ k)

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

Equations

• t.findLongestPrefix? k = Lean.PrefixTree.findLongestPrefix? t (Lean.toKey✝ k)

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

Equations

• t.foldMatchingM 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} [Monad m] (t : NameTrie β) (init : σ) (f : β → σ → m σ) : m σ

Equations

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

@[inline]

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

Equations

• t.forMatchingM k f = Lean.PrefixTree.forMatchingM t (Lean.toKey✝ k) f

@[inline]

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

Equations

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

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

Equations

• t.matchingToArray k = (t.foldMatchingM k #[] fun (v : β) (acc : Array β) => pure (acc.push v)).run

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

Equations

• t.toArray = (t.foldM #[] fun (v : β) (acc : Array β) => pure (acc.push v)).run