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.
@[specialize #[]]
def
Lake.RBNode.dFind
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
[h : Lake.EqOfCmpWrt α β cmp]
:
Lean.RBNode α β → (k : α) → Option (β k)
Equations
- One or more equations did not get rendered due to their size.
- Lake.RBNode.dFind cmp Lean.RBNode.leaf x = none
Instances For
instance
Lake.instCoeDRBMapRBMap
{α : Type u_1}
{β : Type u_2}
{cmp : α → α → Ordering}
:
Coe (Lake.DRBMap α (fun x => β) cmp) (Lean.RBMap α β cmp)
@[inline]
Instances For
@[inline]
Instances For
instance
Lake.instEmptyCollectionDRBMap
(α : Type u)
(β : α → Type v)
(cmp : α → α → Ordering)
:
EmptyCollection (Lake.DRBMap α β cmp)
def
Lake.DRBMap.depth
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
(f : Nat → Nat → Nat)
(t : Lake.DRBMap α β cmp)
:
Instances For
@[inline]
def
Lake.DRBMap.fold
{α : Type u}
{β : α → Type v}
{σ : Type w}
{cmp : α → α → Ordering}
(f : σ → (k : α) → β k → σ)
(init : σ)
:
Lake.DRBMap α β cmp → σ
Instances For
@[inline]
def
Lake.DRBMap.revFold
{α : Type u}
{β : α → Type v}
{σ : Type w}
{cmp : α → α → Ordering}
(f : σ → (k : α) → β k → σ)
(init : σ)
:
Lake.DRBMap α β cmp → σ
Instances For
@[inline]
def
Lake.DRBMap.foldM
{α : Type u}
{β : α → Type v}
{σ : Type w}
{cmp : α → α → Ordering}
{m : Type w → Type u_1}
[Monad m]
(f : σ → (k : α) → β k → m σ)
(init : σ)
:
Lake.DRBMap α β cmp → m σ
Instances For
instance
Lake.DRBMap.instForInDRBMapSigma
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
{m : Type u_1 → Type u_2}
:
ForIn m (Lake.DRBMap α β cmp) ((k : α) × β k)
@[inline]
def
Lake.DRBMap.isEmpty
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → Bool
Instances For
@[specialize #[]]
def
Lake.DRBMap.toList
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → List ((k : α) × β k)
Instances For
@[inline]
def
Lake.DRBMap.min
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → Option ((k : α) × β k)
Instances For
@[inline]
def
Lake.DRBMap.max
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → Option ((k : α) × β k)
Instances For
instance
Lake.DRBMap.instReprDRBMap
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[Repr ((k : α) × β k)]
:
Repr (Lake.DRBMap α β cmp)
@[inline]
def
Lake.DRBMap.insert
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → (k : α) → β k → Lake.DRBMap α β cmp
Instances For
@[inline]
def
Lake.DRBMap.erase
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → α → Lake.DRBMap α β cmp
Instances For
@[specialize #[]]
def
Lake.DRBMap.ofList
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
List ((k : α) × β k) → Lake.DRBMap α β cmp
Equations
- Lake.DRBMap.ofList [] = Lake.mkDRBMap α β cmp
- Lake.DRBMap.ofList ({ fst := k, snd := v } :: xs) = Lake.DRBMap.insert (Lake.DRBMap.ofList xs) k v
Instances For
@[inline]
def
Lake.DRBMap.findCore?
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → α → Option ((k : α) × β k)
Instances For
@[inline]
def
Lake.DRBMap.find?
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[Lake.EqOfCmpWrt α β cmp]
:
Lake.DRBMap α β cmp → (k : α) → Option (β k)
Instances For
@[inline]
def
Lake.DRBMap.findD
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[Lake.EqOfCmpWrt α β cmp]
(t : Lake.DRBMap α β cmp)
(k : α)
(v₀ : β k)
:
β k
Instances For
@[inline]
def
Lake.DRBMap.lowerBound
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → α → Option ((k : α) × β k)
(lowerBound k) retrieves the kv pair of the largest key smaller than or equal to k
,
if it exists.
Instances For
@[inline]
def
Lake.DRBMap.contains
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[Lake.EqOfCmpWrt α β cmp]
(t : Lake.DRBMap α β cmp)
(k : α)
:
Instances For
@[inline]
def
Lake.DRBMap.fromList
{α : Type u}
{β : α → Type v}
(l : List ((k : α) × β k))
(cmp : α → α → Ordering)
:
Lake.DRBMap α β cmp
Instances For
@[inline]
def
Lake.DRBMap.all
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → ((k : α) → β k → Bool) → Bool
Instances For
@[inline]
def
Lake.DRBMap.any
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
:
Lake.DRBMap α β cmp → ((k : α) → β k → Bool) → Bool
Instances For
def
Lake.DRBMap.size
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
(m : Lake.DRBMap α β cmp)
:
Instances For
def
Lake.DRBMap.maxDepth
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
(t : Lake.DRBMap α β cmp)
:
Instances For
@[inline]
def
Lake.DRBMap.min!
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[Inhabited ((k : α) × β k)]
(t : Lake.DRBMap α β cmp)
:
(k : α) × β k
Instances For
@[inline]
def
Lake.DRBMap.max!
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[Inhabited ((k : α) × β k)]
(t : Lake.DRBMap α β cmp)
:
(k : α) × β k
Instances For
@[inline]
def
Lake.DRBMap.find!
{α : Type u}
{β : α → Type v}
{cmp : α → α → Ordering}
[Lake.EqOfCmpWrt α β cmp]
(t : Lake.DRBMap α β cmp)
(k : α)
[Inhabited (β k)]
:
β k
Instances For
def
Lake.drbmapOf
{α : Type u}
{β : α → Type v}
(l : List ((k : α) × β k))
(cmp : α → α → Ordering)
:
Lake.DRBMap α β cmp