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

Equations

• Lean.Data.Trie.empty = Lean.Data.Trie.leaf none

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

Equations

• Lean.Data.Trie.instEmptyCollection = { emptyCollection := Lean.Data.Trie.empty }

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

Equations

• Lean.Data.Trie.instInhabited = { default := Lean.Data.Trie.empty }

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

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

Equations

• t.upsert s f = Lean.Data.Trie.upsert.loop✝ s f 0 t

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.

Equations

• t.insert s val = t.upsert s fun (x : Option α) => val

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

Looks up a value at the given key s.

Equations

• t.find? s = Lean.Data.Trie.find?.loop✝ s 0 t

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

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

Equations

• t.values = (StateT.run (Lean.Data.Trie.values.go✝ t) #[]).snd

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.

Equations

• t.findPrefix pre = Lean.Data.Trie.findPrefix.go✝ pre t 0

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.

Equations

• Lean.Data.Trie.matchPrefix s t i = Lean.Data.Trie.matchPrefix.loop✝ s t i.byteIdx none

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

Equations

• Lean.Data.Trie.instToString = { toString := fun (t : Lean.Data.Trie α) => Lean.Data.Trie.instToString._private_1 t }