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.

instance Lake.inhabitedOfEmptyCollection {α : Type u_1} [EmptyCollection α] : Inhabited α

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

def Lake.DRBMap (α : Type u) (β : α → Type v) (cmp : α → α → Ordering) : Type (max u v)

A Dependently typed RBMap.

@[inline]

def Lake.mkDRBMap (α : Type u) (β : α → Type v) (cmp : α → α → Ordering) : Lake.DRBMap α β cmp

@[inline]

def Lake.DRBMap.empty {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp

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) : Nat

@[inline]

def Lake.DRBMap.fold {α : Type u} {β : α → Type v} {σ : Type w} {cmp : α → α → Ordering} (f : σ → (k : α) → β k → σ) (init : σ) : Lake.DRBMap α β cmp → σ

@[inline]

def Lake.DRBMap.revFold {α : Type u} {β : α → Type v} {σ : Type w} {cmp : α → α → Ordering} (f : σ → (k : α) → β k → σ) (init : σ) : Lake.DRBMap α β cmp → σ

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

@[inline]

def Lake.DRBMap.forM {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} [Monad m] (f : (k : α) → β k → m PUnit) (t : Lake.DRBMap α β cmp) : m PUnit

@[inline]

def Lake.DRBMap.forIn {α : Type u} {β : α → Type v} {σ : Type w} {cmp : α → α → Ordering} {m : Type w → Type u_1} [Monad m] (t : Lake.DRBMap α β cmp) (init : σ) (f : (k : α) × β k → σ → m (ForInStep σ)) : m σ

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

@[specialize #[]]

def Lake.DRBMap.toList {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp → List ((k : α) × β k)

@[inline]

def Lake.DRBMap.min {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp → Option ((k : α) × β k)

@[inline]

def Lake.DRBMap.max {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp → Option ((k : α) × β k)

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

@[inline]

def Lake.DRBMap.erase {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp → α → Lake.DRBMap α β cmp

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

@[inline]

def Lake.DRBMap.findCore? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp → α → Option ((k : α) × β k)

@[inline]

def Lake.DRBMap.find? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Lake.EqOfCmpWrt α β cmp] : Lake.DRBMap α β cmp → (k : α) → Option (β k)

@[inline]

def Lake.DRBMap.findD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Lake.EqOfCmpWrt α β cmp] (t : Lake.DRBMap α β cmp) (k : α) (v₀ : β k) : β k

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

@[inline]

def Lake.DRBMap.contains {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Lake.EqOfCmpWrt α β cmp] (t : Lake.DRBMap α β cmp) (k : α) : Bool

@[inline]

def Lake.DRBMap.fromList {α : Type u} {β : α → Type v} (l : List ((k : α) × β k)) (cmp : α → α → Ordering) : Lake.DRBMap α β cmp

@[inline]

def Lake.DRBMap.all {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp → ((k : α) → β k → Bool) → Bool

@[inline]

def Lake.DRBMap.any {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Lake.DRBMap α β cmp → ((k : α) → β k → Bool) → Bool

def Lake.DRBMap.size {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (m : Lake.DRBMap α β cmp) : Nat

def Lake.DRBMap.maxDepth {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Lake.DRBMap α β cmp) : Nat

@[inline]

def Lake.DRBMap.min! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Inhabited ((k : α) × β k)] (t : Lake.DRBMap α β cmp) : (k : α) × β k

@[inline]

def Lake.DRBMap.max! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Inhabited ((k : α) × β k)] (t : Lake.DRBMap α β cmp) : (k : α) × β k

@[inline]

def Lake.DRBMap.find! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Lake.EqOfCmpWrt α β cmp] (t : Lake.DRBMap α β cmp) (k : α) [Inhabited (β k)] : β k

def Lake.drbmapOf {α : Type u} {β : α → Type v} (l : List ((k : α) × β k)) (cmp : α → α → Ordering) : Lake.DRBMap α β cmp