inductive Lean.PrefixTreeNode (α : Type u) (β : Type v) : Type (max u v)

• Node {α : Type u} {β : Type v} : Option β → (RBNode α fun (x : α) => PrefixTreeNode α β) → PrefixTreeNode α β

instance Lean.instInhabitedPrefixTreeNode {α : Type u_1} {β : Type u_2} : Inhabited (PrefixTreeNode α β)

def Lean.PrefixTreeNode.empty {α : Type u_1} {β : Type u_2} : PrefixTreeNode α β

@[specialize #[]]

def Lean.PrefixTreeNode.insert {α : Type u_1} {β : Type u_2} (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (val : β) : PrefixTreeNode α β

partial def Lean.PrefixTreeNode.insert.insertEmpty {α : Type u_1} {β : Type u_2} (val : β) (k : List α) : PrefixTreeNode α β

partial def Lean.PrefixTreeNode.insert.loop {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (val : β) : PrefixTreeNode α β → List α → PrefixTreeNode α β

@[specialize #[]]

def Lean.PrefixTreeNode.find? {α : Type u_1} {β : Type u_2} (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) : Option β

partial def Lean.PrefixTreeNode.find?.loop {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) : PrefixTreeNode α β → List α → Option β

@[specialize #[]]

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

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

partial def Lean.PrefixTreeNode.findLongestPrefix?.loop {α : Type u_1} {β : Type u_2} (cmp : α → α → Ordering) (acc? : Option β) : PrefixTreeNode α β → List α → Option β

@[specialize #[]]

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

partial def Lean.PrefixTreeNode.foldMatchingM.fold {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {σ : Type u_1} [Monad m] (f : β → σ → m σ) : PrefixTreeNode α β → σ → m σ

partial def Lean.PrefixTreeNode.foldMatchingM.find {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {σ : Type u_1} [Monad m] (cmp : α → α → Ordering) (init : σ) (f : β → σ → m σ) : List α → PrefixTreeNode α β → σ → m σ

inductive Lean.PrefixTreeNode.WellFormed {α : Type u_1} (cmp : α → α → Ordering) {β : Type u_2} : PrefixTreeNode α β → 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✝} {k : List α} {val : x✝} : WellFormed cmp t → WellFormed cmp (t.insert cmp k val)

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

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

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

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

@[inline]

def Lean.PrefixTree.insert {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} (t : PrefixTree α β p) (k : List α) (v : β) : PrefixTree α β p

@[inline]

def Lean.PrefixTree.find? {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} (t : PrefixTree α β p) (k : List α) : Option β

@[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.

@[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 σ

@[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 σ

@[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

@[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