# The `Cell` type #

source
structure Std.DTreeMap.Internal.Cell (α : Type u) [Ord α] (β : α → Type v) (k : α → Ordering) :
Type (max u v)

Type for representing the place in a tree map where a mapping for `k` could live. Internal implementation detail of the tree map.

- inner : Option ((a : α) × β a)

  The mapping.

- property [OrientedOrd α] (p : (a : α) × β a) : self.inner = some p → k p.fst = Ordering.eq

  If there is a mapping, then it has a matching key.

Instances For

source
def Std.DTreeMap.Internal.Cell.ofEq {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} (k' : α) (v' : β k') (hcmp : ∀ [OrientedOrd α], k k' = Ordering.eq) :
Cell α β k

Create a cell with a matching key. Internal implementation detail of the tree map

Equations

- Std.DTreeMap.Internal.Cell.ofEq k' v' hcmp = { inner := some ⟨k', v'⟩, property := ⋯ }

Instances For

source
def Std.DTreeMap.Internal.Cell.of {α : Type u} {β : α → Type v} [Ord α] (k : α) (v : β k) :
Cell α β (compare k)

Create a cell with a matching key. Internal implementation detail of the tree map

Equations

- Std.DTreeMap.Internal.Cell.of k v = Std.DTreeMap.Internal.Cell.ofEq k v ⋯

Instances For

source
@[simp]
theorem Std.DTreeMap.Internal.Cell.ofEq_inner {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} {k' : α} {v' : β k'} {h : ∀ [OrientedOrd α], k k' = Ordering.eq} :
(ofEq k' v' h).inner = some ⟨k', v'⟩
source
@[simp]
theorem Std.DTreeMap.Internal.Cell.of_inner {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} :
(of k v).inner = some ⟨k, v⟩
source
def Std.DTreeMap.Internal.Cell.empty {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} :
Cell α β k

Create an empty cell. Internal implementation detail of the tree map

Equations

- Std.DTreeMap.Internal.Cell.empty = { inner := none, property := ⋯ }

Instances For

source
def Std.DTreeMap.Internal.Cell.ofOption {α : Type u} {β : α → Type v} [Ord α] (k : α) (v? : Option (β k)) :
Cell α β (compare k)

Internal implementation detail of the tree map

Equations

- Std.DTreeMap.Internal.Cell.ofOption k none = Std.DTreeMap.Internal.Cell.empty
- Std.DTreeMap.Internal.Cell.ofOption k (some v) = Std.DTreeMap.Internal.Cell.of k v

Instances For

source
@[simp]
theorem Std.DTreeMap.Internal.Cell.empty_inner {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} :
empty.inner = none
source
def Std.DTreeMap.Internal.Cell.contains {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} (c : Cell α β k) :
Bool

Internal implementation detail of the tree map

Equations

- c.contains = c.inner.isSome

Instances For

source
@[simp]
theorem Std.DTreeMap.Internal.Cell.contains_of {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} :
(of k v).contains = true
source
@[simp]
theorem Std.DTreeMap.Internal.Cell.contains_ofEq {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} {k' : α} {v' : β k'} {h : ∀ [OrientedOrd α], k k' = Ordering.eq} :
(ofEq k' v' h).contains = true
source
@[simp]
theorem Std.DTreeMap.Internal.Cell.contains_empty {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} :
empty.contains = false
source
theorem Std.DTreeMap.Internal.Cell.containsKey_inner_toList {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {c : Cell α β (compare k)} :
c.contains = true → Internal.List.containsKey k c.inner.toList = true
source
def Std.DTreeMap.Internal.Cell.get? {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} (c : Cell α β (compare k)) :
Option (β k)

Internal implementation detail of the tree map

Equations

- c.get? = match h : c.inner with | none => none | some p => some (cast ⋯ p.snd)

Instances For

source
@[simp]
theorem Std.DTreeMap.Internal.Cell.get?_empty {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} :
empty.get? = none
source
def Std.DTreeMap.Internal.Cell.getKey? {α : Type u} {β : α → Type v} [Ord α] {k : α} (c : Cell α β (compare k)) :
Option α

Internal implementation detail of the tree map

Equations

- c.getKey? = match c.inner with | none => none | some p => some p.fst

Instances For

source
@[simp]
theorem Std.DTreeMap.Internal.Cell.getKey?_empty {α : Type u} {β : α → Type v} [Ord α] {k : α} :
empty.getKey? = none
source
def Std.DTreeMap.Internal.Cell.alter {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} (f : Option (β k) → Option (β k)) (c : Cell α β (compare k)) :
Cell α β (compare k)

Internal implementation detail of the tree map

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Std.DTreeMap.Internal.Cell.ext {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} {c c' : Cell α β k} :
c.inner = c'.inner → c = c'
source
def Std.DTreeMap.Internal.Cell.Const.get? {α : Type u} {β : Type v} [Ord α] {k : α} (c : Cell α (fun (x : α) => β) (compare k)) :
Option β

Internal implementation detail of the tree map

Equations

- Std.DTreeMap.Internal.Cell.Const.get? c = match c.inner with | none => none | some p => some p.snd

Instances For

source
@[simp]
theorem Std.DTreeMap.Internal.Cell.Const.get?_empty {α : Type u} {β : Type v} [Ord α] {k : α} :
get? empty = none
source
def Std.DTreeMap.Internal.Cell.Const.alter {α : Type u} {β : Type v} [Ord α] [OrientedOrd α] {k : α} (f : Option β → Option β) (c : Cell α (fun (x : α) => β) (compare k)) :
Cell α (fun (x : α) => β) (compare k)

Internal implementation detail of the tree map

Equations

- Std.DTreeMap.Internal.Cell.Const.alter f c = match c.inner with | none => Std.DTreeMap.Internal.Cell.ofOption k (f none) | some ⟨fst, v'⟩ => Std.DTreeMap.Internal.Cell.ofOption k (f (some v'))

Instances For

source
def Std.DTreeMap.Internal.List.findCell {α : Type u} {β : α → Type v} [Ord α] (l : List ((a : α) × β a)) (k : α → Ordering) :
Cell α β k

Internal implementation detail of the tree map

Equations

- Std.DTreeMap.Internal.List.findCell l k = { inner := List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l, property := ⋯ }

Instances For

source
theorem Std.DTreeMap.Internal.List.findCell_inner {α : Type u} {β : α → Type v} [Ord α] (l : List ((a : α) × β a)) (k : α → Ordering) :
(findCell l k).inner = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l
source
@[simp]
theorem Std.DTreeMap.Internal.List.findCell_nil {α : Type u} {β : α → Type v} [Ord α] (k : α → Ordering) :
findCell [] k = Cell.empty