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 α → Lean.Data.Trie α
• node1: {α : Type} → Option α → UInt8 → Lean.Data.Trie α → Lean.Data.Trie α
• node: {α : Type} → Option α → ByteArray → Array (Lean.Data.Trie α) → Lean.Data.Trie α

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

The empty Trie

Equations

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

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

Equations

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

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

Equations

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

def Lean.Data.Trie.upsert {α : Type} (t : Lean.Data.Trie α) (s : String) (f : Option α → α) : Lean.Data.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

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

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

def Lean.Data.Trie.insert {α : Type} (t : Lean.Data.Trie α) (s : String) (val : α) : Lean.Data.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 : Lean.Data.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

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

def Lean.Data.Trie.values {α : Type} (t : Lean.Data.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

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

def Lean.Data.Trie.findPrefix {α : Type} (t : Lean.Data.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

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

def Lean.Data.Trie.matchPrefix {α : Type} (s : String) (t : Lean.Data.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

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

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

Equations

• Lean.Data.Trie.instToString = { toString := fun (t : Lean.Data.Trie α) => (flip Lean.Format.joinSep Lean.Format.line (Lean.Data.Trie.toStringAux t)).pretty }