Documentation

Lean.Data.Trie

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

Type

Node: {α : Type} → Option α → (Std.RBNode Char fun x => Lean.Parser.Trie α) → Lean.Parser.Trie α

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

Lean.Parser.Trie α

Equations

Lean.Parser.Trie.empty = Lean.Parser.Trie.Node none Std.RBNode.leaf

instance Lean.Parser.Trie.instEmptyCollectionTrie {α : Type} :

EmptyCollection (Lean.Parser.Trie α)

Equations

Lean.Parser.Trie.instEmptyCollectionTrie = { emptyCollection := Lean.Parser.Trie.empty }

instance Lean.Parser.Trie.instInhabitedTrie {α : Type} :

Inhabited (Lean.Parser.Trie α)

Equations

Lean.Parser.Trie.instInhabitedTrie = { default := Lean.Parser.Trie.Node none Std.RBNode.leaf }

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

Lean.Parser.Trie α

Equations

Lean.Parser.Trie.insert t s val = (fun insertEmpty => (fun loop => loop t 0) (Lean.Parser.Trie.insert.loop s val)) (Lean.Parser.Trie.insert.insertEmpty s val)

partial def Lean.Parser.Trie.insert.insertEmpty {α : Type} (s : String) (val : α) (i : String.Pos) :

Lean.Parser.Trie α

partial def Lean.Parser.Trie.insert.loop {α : Type} (s : String) (val : α) :

Lean.Parser.Trie α → String.Pos → Lean.Parser.Trie α

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

Equations

Lean.Parser.Trie.find? t s = (fun loop => loop t 0) (Lean.Parser.Trie.find?.loop s)

partial def Lean.Parser.Trie.find?.loop {α : Type} (s : String) :

Lean.Parser.Trie α → String.Pos → Option α

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

Equations

Lean.Parser.Trie.findPrefix t pre = (fun go collect => (StateT.run (go t 0) #[]).snd) (Lean.Parser.Trie.findPrefix.go pre) Lean.Parser.Trie.findPrefix.collect

partial def Lean.Parser.Trie.findPrefix.go {α : Type} (pre : String) (t : Lean.Parser.Trie α) (i : String.Pos) :

StateM (Array α) Unit

partial def Lean.Parser.Trie.findPrefix.collect {α : Type} (t : Lean.Parser.Trie α) :

StateM (Array α) Unit

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

String.Pos × Option α

Equations

Lean.Parser.Trie.matchPrefix s t i = (fun loop => loop t i (i, none)) (Lean.Parser.Trie.matchPrefix.loop s)

partial def Lean.Parser.Trie.matchPrefix.loop {α : Type} (s : String) :

Lean.Parser.Trie α → String.Pos → String.Pos × Option α → String.Pos × Option α

instance Lean.Parser.Trie.instToStringTrie {α : Type} :

ToString (Lean.Parser.Trie α)

Equations

Lean.Parser.Trie.instToStringTrie = { toString := fun t => Lean.Format.pretty (flip Lean.Format.joinSep Lean.Format.line (Lean.Parser.Trie.toStringAux t)) }