source
inductive Lean.PrefixTreeNode (α : Type u) (β : Type v) (cmp : α → α → Ordering) :
Type (max u v)

- Node {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Option β → Std.TreeMap.Raw α (PrefixTreeNode α β cmp) cmp → PrefixTreeNode α β cmp

Instances For

source
instance Lean.instInhabitedPrefixTreeNode {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} :
Inhabited (PrefixTreeNode α β cmp)
Equations

- Lean.instInhabitedPrefixTreeNode = { default := Lean.PrefixTreeNode.Node none ∅ }

source
def Lean.PrefixTreeNode.empty {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} :
PrefixTreeNode α β cmp
Equations

- Lean.PrefixTreeNode.empty = Lean.PrefixTreeNode.Node none ∅

Instances For

source
@[inline]
def Lean.PrefixTreeNode.insert {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) (val : β) :
PrefixTreeNode α β cmp
Equations

- Lean.PrefixTreeNode.insert cmp t k val = Lean.PrefixTreeNode.insert.loop✝ cmp val t k

Instances For

source
@[specialize #[]]
def Lean.PrefixTreeNode.find? {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) :
Option β
Equations

- Lean.PrefixTreeNode.find? cmp t k = Lean.PrefixTreeNode.find?.loop✝ cmp t k

Instances For

source
@[inline]
def Lean.PrefixTreeNode.findLongestPrefix? {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) :
Option β

Returns the the value of the longest key in `t` that is a prefix of `k`, if any.

Equations

- Lean.PrefixTreeNode.findLongestPrefix? cmp t k = Lean.PrefixTreeNode.findLongestPrefix?.loop✝ cmp none t k

Instances For

source
@[inline]
def Lean.PrefixTreeNode.foldMatchingM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {σ : Type u_1} [Monad m] (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) (init : σ) (f : β → σ → m σ) :
m σ
Equations

- Lean.PrefixTreeNode.foldMatchingM cmp t k init f = Lean.PrefixTreeNode.foldMatchingM.find✝ cmp init f k t init

Instances For

source
inductive Lean.PrefixTreeNode.WellFormed {α : Type u_1} (cmp : α → α → Ordering) {β : Type u_2} :
PrefixTreeNode α β cmp → Prop

- emptyWff {α : Type u_1} {cmp : α → α → Ordering} {x✝ : Type u_2} : WellFormed cmp empty
- insertWff {α : Type u_1} {cmp : α → α → Ordering} {x✝ : Type u_2} {t : PrefixTreeNode α x✝ cmp} {k : List α} {val : x✝} : WellFormed cmp t → WellFormed cmp (insert cmp t k val)

Instances For

source
def Lean.PrefixTree (α : Type u) (β : Type v) (cmp : α → α → Ordering) :
Type (max u v)
Equations

- Lean.PrefixTree α β cmp = { t : Lean.PrefixTreeNode α β cmp // Lean.PrefixTreeNode.WellFormed cmp t }

Instances For

source
def Lean.PrefixTree.empty {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} :
PrefixTree α β p
Equations

- Lean.PrefixTree.empty = ⟨Lean.PrefixTreeNode.empty, ⋯⟩

Instances For

source
instance Lean.instInhabitedPrefixTree {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} :
Inhabited (PrefixTree α β p)
Equations

- Lean.instInhabitedPrefixTree = { default := Lean.PrefixTree.empty }

source
instance Lean.instEmptyCollectionPrefixTree {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} :
EmptyCollection (PrefixTree α β p)
Equations

- Lean.instEmptyCollectionPrefixTree = { emptyCollection := Lean.PrefixTree.empty }

source
@[inline]
def Lean.PrefixTree.insert {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} (t : PrefixTree α β p) (k : List α) (v : β) :
PrefixTree α β p
Equations

- t.insert k v = ⟨Lean.PrefixTreeNode.insert p t.val k v, ⋯⟩

Instances For

source
@[inline]
def Lean.PrefixTree.find? {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} (t : PrefixTree α β p) (k : List α) :
Option β
Equations

- t.find? k = Lean.PrefixTreeNode.find? p t.val k

Instances For

source
@[inline]
def Lean.PrefixTree.findLongestPrefix? {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} (t : PrefixTree α β p) (k : List α) :
Option β

Returns the the value of the longest key in `t` that is a prefix of `k`, if any.

Equations

- t.findLongestPrefix? k = Lean.PrefixTreeNode.findLongestPrefix? p t.val k

Instances For

source
@[inline]
def Lean.PrefixTree.foldMatchingM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {p : α → α → Ordering} {σ : Type u_1} [Monad m] (t : PrefixTree α β p) (k : List α) (init : σ) (f : β → σ → m σ) :
m σ
Equations

- t.foldMatchingM k init f = Lean.PrefixTreeNode.foldMatchingM p t.val k init f

Instances For

source
@[inline]
def Lean.PrefixTree.foldM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {p : α → α → Ordering} {σ : Type u_1} [Monad m] (t : PrefixTree α β p) (init : σ) (f : β → σ → m σ) :
m σ
Equations

- t.foldM init f = t.foldMatchingM [] init f

Instances For

source
@[inline]
def Lean.PrefixTree.forMatchingM {m : Type → Type u_1} {α : Type u_2} {β : Type u_3} {p : α → α → Ordering} [Monad m] (t : PrefixTree α β p) (k : List α) (f : β → m Unit) :
m Unit
Equations

- t.forMatchingM k f = Lean.PrefixTreeNode.foldMatchingM p t.val k () fun (b : β) (x : Unit) => f b

Instances For

source
@[inline]
def Lean.PrefixTree.forM {m : Type → Type u_1} {α : Type u_2} {β : Type u_3} {p : α → α → Ordering} [Monad m] (t : PrefixTree α β p) (f : β → m Unit) :
m Unit
Equations

- t.forM f = t.forMatchingM [] f

Instances For