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.

partial def Lean.Data.Trie.upsert.insertEmpty {α : Type} (s : String) (f : Option α → α) (i : Nat) : Trie α

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

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.

partial def Lean.Data.Trie.find?.loop {α : Type} (s : String) : Nat → Trie α → Option α

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

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

partial def Lean.Data.Trie.values.go {α : Type} : Trie α → StateM (Array α) Unit

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.

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

def Lean.Data.Trie.matchPrefix {α : Type} (s : String) (t : Trie α) (i : String.Pos) : Option α

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

partial def Lean.Data.Trie.matchPrefix.loop {α : Type} (s : String) : Trie α → Nat → Option α → Option α

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