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.
If there is a mapping, then it has a matching key.
Instances For
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
Instances For
@[simp]
theorem
Std.DTreeMap.Internal.Cell.ofEq_inner
{α : Type u}
{β : α → Type v}
[Ord α]
{k : α → Ordering}
{k' : α}
{v' : β k'}
{h : ∀ [OrientedOrd α], k k' = Ordering.eq}
:
@[simp]
theorem
Std.DTreeMap.Internal.Cell.contains_ofEq
{α : Type u}
{β : α → Type v}
[Ord α]
{k : α → Ordering}
{k' : α}
{v' : β k'}
{h : ∀ [OrientedOrd α], k k' = Ordering.eq}
:
theorem
Std.DTreeMap.Internal.Cell.containsKey_inner_toList
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[BEq α]
[LawfulBEqOrd α]
{k : α}
{c : Cell α β (compare k)}
:
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
Instances For
@[simp]
theorem
Std.DTreeMap.Internal.Cell.get?_empty
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
{k : α}
:
def
Std.DTreeMap.Internal.Cell.alter
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
{k : α}
(f : Option (β k) → Option (β k))
(c : Cell α β (compare k))
:
Internal implementation detail of the tree map