The Cell type

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.

def Std.DTreeMap.Internal.Cell.ofEq {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} (k' : α) (v' : β k') (hcmp : ∀ [inst : 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 := ⋯ }

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 ⋯

@[simp]

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

@[simp]

theorem Std.DTreeMap.Internal.Cell.of_inner {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} : (of k v).inner = some ⟨k, v⟩

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 := ⋯ }

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

@[simp]

theorem Std.DTreeMap.Internal.Cell.empty_inner {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} : empty.inner = none

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

@[simp]

theorem Std.DTreeMap.Internal.Cell.contains_of {α : Type u} {β : α → Type v} [Ord α] {k : α} {v : β k} : (of k v).contains = true

@[simp]

theorem Std.DTreeMap.Internal.Cell.contains_ofEq {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} {k' : α} {v' : β k'} {h : ∀ [inst : OrientedOrd α], k k' = Ordering.eq} : (ofEq k' v' h).contains = true

@[simp]

theorem Std.DTreeMap.Internal.Cell.contains_empty {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} : empty.contains = false

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

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)

@[simp]

theorem Std.DTreeMap.Internal.Cell.get?_empty {α : Type u} {β : α → Type v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} : empty.get? = none

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

@[simp]

theorem Std.DTreeMap.Internal.Cell.getKey?_empty {α : Type u} {β : α → Type v} [Ord α] {k : α} : empty.getKey? = none

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.

theorem Std.DTreeMap.Internal.Cell.ext {α : Type u} {β : α → Type v} [Ord α] {k : α → Ordering} {c c' : Cell α β k} : c.inner = c'.inner → c = c'

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

@[simp]

theorem Std.DTreeMap.Internal.Cell.Const.get?_empty {α : Type u} {β : Type v} [Ord α] {k : α} : get? empty = none

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'))

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 := ⋯ }

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

@[simp]

theorem Std.DTreeMap.Internal.List.findCell_nil {α : Type u} {β : α → Type v} [Ord α] (k : α → Ordering) : findCell [] k = Cell.empty