Lean.Data.PrefixTree

source

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

Type (max u v)

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

source

instance Lean.instInhabitedPrefixTreeNode {α : Type u_1} {β : Type u_2} :

Inhabited (Lean.PrefixTreeNode α β)

Equations

Lean.instInhabitedPrefixTreeNode = { default := Lean.PrefixTreeNode.Node none Std.RBNode.leaf }

source

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

Lean.PrefixTreeNode α β

Equations

Lean.PrefixTreeNode.empty = Lean.PrefixTreeNode.Node none Std.RBNode.leaf

source

@[specialize]

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

Lean.PrefixTreeNode α β

Equations

Lean.PrefixTreeNode.insert t cmp k val = (fun insertEmpty => (fun loop => loop t k) (Lean.PrefixTreeNode.insert.loop cmp val)) (Lean.PrefixTreeNode.insert.insertEmpty val)

source

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

Lean.PrefixTreeNode α β

source

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

Lean.PrefixTreeNode α β → List α → Lean.PrefixTreeNode α β

source

@[specialize]

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

Option β

Equations

Lean.PrefixTreeNode.find? t cmp k = (fun loop => loop t k) (Lean.PrefixTreeNode.find?.loop cmp)

source

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

Lean.PrefixTreeNode α β → List α → Option β

source

@[specialize]

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

m σ

Equations

Lean.PrefixTreeNode.foldMatchingM t cmp k init f = (fun fold => (fun find => find k t init) (Lean.PrefixTreeNode.foldMatchingM.find cmp init f)) (Lean.PrefixTreeNode.foldMatchingM.fold f)

source

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

Lean.PrefixTreeNode α β → σ → m σ

source

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

List α → Lean.PrefixTreeNode α β → σ → m σ

source

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

Lean.PrefixTreeNode α β → Prop

emptyWff: ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering}, Lean.PrefixTreeNode.WellFormed cmp Lean.PrefixTreeNode.empty
insertWff: ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : Lean.PrefixTreeNode α β} {k : List α} {val : β}, Lean.PrefixTreeNode.WellFormed cmp t → Lean.PrefixTreeNode.WellFormed cmp (Lean.PrefixTreeNode.insert t cmp k val)

source

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

Type (max u v)

Equations

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

source

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

Lean.PrefixTree α β p

Equations

Lean.PrefixTree.empty = { val := Lean.PrefixTreeNode.empty, property := (_ : Lean.PrefixTreeNode.WellFormed p Lean.PrefixTreeNode.empty) }

source

instance Lean.instInhabitedPrefixTree {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} :

Inhabited (Lean.PrefixTree α β p)

Equations

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

source

instance Lean.instEmptyCollectionPrefixTree {α : Type u_1} {β : Type u_2} {p : α → α → Ordering} :

EmptyCollection (Lean.PrefixTree α β p)

Equations

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

source

@[inline]

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

Lean.PrefixTree α β p

Equations

Lean.PrefixTree.insert t k v = { val := Lean.PrefixTreeNode.insert t.val p k v, property := (_ : Lean.PrefixTreeNode.WellFormed p (Lean.PrefixTreeNode.insert t.val p k v)) }

source

@[inline]

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

Option β

Equations

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

source

@[inline]

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

m σ

Equations

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

source

@[inline]

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

m σ

Equations

Lean.PrefixTree.foldM t init f = Lean.PrefixTree.foldMatchingM t [] init f

source

@[inline]

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

m Unit

Equations

Lean.PrefixTree.forMatchingM t k f = Lean.PrefixTreeNode.foldMatchingM t.val p k () fun b x => f b

source

@[inline]

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

m Unit

Equations

Lean.PrefixTree.forM t f = Lean.PrefixTree.forMatchingM t [] f