Lake.Util.DRBMap

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.

source

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

Inhabited α

Equations

Lake.inhabitedOfEmptyCollection = { default := ∅ }

source

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

source

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

Type (max u v)

A Dependently typed RBMap.

Equations

Lake.DRBMap α β cmp = { t : Lean.RBNode α β // Lean.RBNode.WellFormed cmp t }

Instances For

source

instance Lake.instCoeDRBMapRBMap {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} :

Coe (Lake.DRBMap α (fun (x : α) => β) cmp) (Lean.RBMap α β cmp)

Equations

Lake.instCoeDRBMapRBMap = { coe := id }

source

@[inline]

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

Lake.DRBMap α β cmp

Equations

Lake.mkDRBMap α β cmp = ⟨Lean.RBNode.leaf, ⋯⟩

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp

Equations

Lake.DRBMap.empty = Lake.mkDRBMap α β cmp

Instances For

source

instance Lake.instEmptyCollectionDRBMap (α : Type u) (β : α → Type v) (cmp : α → α → Ordering) :

EmptyCollection (Lake.DRBMap α β cmp)

Equations

Lake.instEmptyCollectionDRBMap α β cmp = { emptyCollection := Lake.DRBMap.empty }

source

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

Nat

Equations

Lake.DRBMap.depth f t = Lean.RBNode.depth f t.val

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → σ

Equations

Lake.DRBMap.fold f x✝ x = match x✝, x with | b, ⟨t, property⟩ => Lean.RBNode.fold f b t

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → σ

Equations

Lake.DRBMap.revFold f x✝ x = match x✝, x with | b, ⟨t, property⟩ => Lean.RBNode.revFold f b t

Instances For

source

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

Equations

Lake.DRBMap.foldM f x✝ x = match x✝, x with | b, ⟨t, property⟩ => Lean.RBNode.foldM f b t

Instances For

source

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

Equations

Lake.DRBMap.forM f t = Lake.DRBMap.foldM (fun (x : PUnit) (k : α) (v : β k) => f k v) PUnit.unit t

Instances For

source

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

Equations

t.forIn init f = t.val.forIn init fun (a : α) (b : β a) (acc : σ) => f ⟨a, b⟩ acc

Instances For

source

instance Lake.DRBMap.instForInSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type u_1 → Type u_2} :

ForIn m (Lake.DRBMap α β cmp) ((k : α) × β k)

Equations

Lake.DRBMap.instForInSigma = { forIn := fun {β_1 : Type u_1} [Monad m] => Lake.DRBMap.forIn }

source

@[inline]

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

Lake.DRBMap α β cmp → Bool

Equations

x.isEmpty = match x with | ⟨Lean.RBNode.leaf, property⟩ => true | x => false

Instances For

source

@[specialize #[]]

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

Lake.DRBMap α β cmp → List ((k : α) × β k)

Equations

x.toList = match x with | ⟨t, property⟩ => Lean.RBNode.revFold (fun (ps : List ((k : α) × β k)) (k : α) (v : β k) => ⟨k, v⟩ :: ps) [] t

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → Option ((k : α) × β k)

Equations

x.min = match x with | ⟨t, property⟩ => match t.min with | some ⟨k, v⟩ => some ⟨k, v⟩ | none => none

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → Option ((k : α) × β k)

Equations

x.max = match x with | ⟨t, property⟩ => match t.max with | some ⟨k, v⟩ => some ⟨k, v⟩ | none => none

Instances For

source

instance Lake.DRBMap.instReprOfSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Repr ((k : α) × β k)] :

Repr (Lake.DRBMap α β cmp)

Equations

Lake.DRBMap.instReprOfSigma = { reprPrec := fun (m : Lake.DRBMap α β cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "Lake.drbmapOf " ++ repr m.toList) prec }

source

@[inline]

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

Lake.DRBMap α β cmp → (k : α) → β k → Lake.DRBMap α β cmp

Equations

x✝¹.insert x✝ x = match x✝¹, x✝, x with | ⟨t, w⟩, k, v => ⟨Lean.RBNode.insert cmp t k v, ⋯⟩

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → α → Lake.DRBMap α β cmp

Equations

x✝.erase x = match x✝, x with | ⟨t, w⟩, k => ⟨Lean.RBNode.erase cmp k t, ⋯⟩

Instances For

source

@[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 (⟨k, v⟩ :: xs) = (Lake.DRBMap.ofList xs).insert k v

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → α → Option ((k : α) × β k)

Equations

x✝.findCore? x = match x✝, x with | ⟨t, property⟩, x => Lean.RBNode.findCore cmp t x

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → (k : α) → Option (β k)

Equations

x✝.find? x = match x✝, x with | ⟨t, property⟩, x => Lake.RBNode.dFind cmp t x

Instances For

source

@[inline]

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

β k

Equations

t.findD k v₀ = (t.find? k).getD v₀

Instances For

source

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

Equations

x✝.lowerBound x = match x✝, x with | ⟨t, property⟩, x => Lean.RBNode.lowerBound cmp t x none

Instances For

source

@[inline]

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

Bool

Equations

t.contains k = (t.find? k).isSome

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp

Equations

Lake.DRBMap.fromList l cmp = List.foldl (fun (r : Lake.DRBMap α β cmp) (p : (k : α) × β k) => r.insert p.fst p.snd) (Lake.mkDRBMap α β cmp) l

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → ((k : α) → β k → Bool) → Bool

Equations

x✝.all x = match x✝, x with | ⟨t, property⟩, p => Lean.RBNode.all p t

Instances For

source

@[inline]

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

Lake.DRBMap α β cmp → ((k : α) → β k → Bool) → Bool

Equations

x✝.any x = match x✝, x with | ⟨t, property⟩, p => Lean.RBNode.any p t

Instances For

source

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

Nat

Equations

m.size = Lake.DRBMap.fold (fun (sz : Nat) (x : α) (x : β x) => sz + 1) 0 m

Instances For

source

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

Nat

Equations

t.maxDepth = Lean.RBNode.depth Nat.max t.val

Instances For

source

@[inline]

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

(k : α) × β k

Equations

t.min! = match t.min with | some p => p | none => panicWithPosWithDecl "Lake.Util.DRBMap" "Lake.DRBMap.min!" 136 14 "map is empty"

Instances For

source

@[inline]

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

(k : α) × β k

Equations

t.max! = match t.max with | some p => p | none => panicWithPosWithDecl "Lake.Util.DRBMap" "Lake.DRBMap.max!" 141 14 "map is empty"

Instances For

source

@[inline]

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

β k

Equations

t.find! k = match t.find? k with | some b => b | none => panicWithPosWithDecl "Lake.Util.DRBMap" "Lake.DRBMap.find!" 146 14 "key is not in the map"

Instances For

source

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

Lake.DRBMap α β cmp

Equations

Lake.drbmapOf l cmp = Lake.DRBMap.fromList l cmp

Instances For