This module includes a dependently typed adaption of the Lean.RBMap
defined in Lean.Data.RBMap
module of the Lean core. Most of the code is
copied directly from there with only minor edits.
Equations
@[specialize #[]]
def
Lake.RBNode.dFind
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
[h : EqOfCmpWrt α β cmp]
:
Lean.RBNode α β → (k : α) → Option (β k)
Equations
Instances For
instance
Lake.instCoeDRBMapRBMap
{α : Type u_1}
{β : Type u_2}
{cmp : α → α → Ordering}
:
Coe (DRBMap α (fun (x : α) => β) cmp) (Lean.RBMap α β cmp)
Equations
instance
Lake.instEmptyCollectionDRBMap
(α : Type u)
(β : α → Type v)
(cmp : α → α → Ordering)
:
EmptyCollection (DRBMap α β cmp)
Equations
@[inline]
Equations
Instances For
@[inline]
def
Lake.DRBMap.findD
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[EqOfCmpWrt α β cmp]
(t : DRBMap α β cmp)
(k : α)
(v₀ : β k)
:
β k
Equations
Instances For
@[inline]
def
Lake.DRBMap.contains
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[EqOfCmpWrt α β cmp]
(t : DRBMap α β cmp)
(k : α)
:
Equations
Instances For
@[inline]
def
Lake.DRBMap.find!
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[EqOfCmpWrt α β cmp]
(t : DRBMap α β cmp)
(k : α)
[Inhabited (β k)]
:
β k