inductive Lean.Data.Trie (α : Type) : Type

A Trie is a key-value store where the keys are of type String, and the internal structure is a tree that branches on the bytes of the string.

• leaf {α : Type} : Option α → Trie α
• node1 {α : Type} : Option α → UInt8 → Trie α → Trie α
• node {α : Type} : Option α → ByteArray → Array (Trie α) → Trie α

def Lean.Data.Trie.empty {α : Type} : Trie α

The empty Trie

instance Lean.Data.Trie.instEmptyCollection {α : Type} : EmptyCollection (Trie α)

instance Lean.Data.Trie.instInhabited {α : Type} : Inhabited (Trie α)

def Lean.Data.Trie.upsert {α : Type} (t : Trie α) (s : String) (f : Option α → α) : Trie α

Insert or update the value at a the given key s.

def Lean.Data.Trie.insert {α : Type} (t : Trie α) (s : String) (val : α) : Trie α

Inserts a value at a the given key s, overriding an existing value if present.

def Lean.Data.Trie.find? {α : Type} (t : Trie α) (s : String) : Option α

Looks up a value at the given key s.

def Lean.Data.Trie.values {α : Type} (t : Trie α) : Array α

Returns an Array of all values in the trie, in no particular order.

def Lean.Data.Trie.findPrefix {α : Type} (t : Trie α) (pre : String) : Array α

Returns all values whose key have the given string pre as a prefix, in no particular order.

def Lean.Data.Trie.matchPrefix {α : Type} (s : String) (t : Trie α) (i : String.Pos.Raw) (endByte : Nat := s.utf8ByteSize) (endByte_valid : endByte ≤ s.utf8ByteSize := by simp) : Option α

Find the longest key in the trie that is contained in the given string s at position i, and return the associated value.

instance Lean.Data.Trie.instToString {α : Type} : ToString (Trie α)