Documentation

Lean.Data.Trie

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

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

Instances For

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

Lean.Parser.Trie α

Instances For

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

EmptyCollection (Lean.Parser.Trie α)

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

Inhabited (Lean.Parser.Trie α)

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

Lean.Parser.Trie α

Instances For

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) :

Instances For

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) :

Return values that match the given prefix

Instances For

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 α

Instances For

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 α)