This module provides slice notation for TreeMap slices and implements an iterator
for those slices.
instance
Std.DTreeMap.Raw.instSliceableRiiSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Rii.Sliceable (Raw α β cmp) α (Internal.RiiSlice α β)
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Std.DTreeMap.Raw.toList_rii
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
{t : Raw α β cmp}
:
instance
Std.DTreeMap.Raw.instSliceableRicSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Ric.Sliceable (Raw α β cmp) α (Internal.RicSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_ric
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun (e : (a : α) × β a) => (cmp e.fst bound).isLE) t.toList
instance
Std.DTreeMap.Raw.instSliceableRioSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Rio.Sliceable (Raw α β cmp) α (Internal.RioSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_rio
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Rio.Sliceable.mkSlice t *...bound) = List.filter (fun (e : (a : α) × β a) => (cmp e.fst bound).isLT) t.toList
instance
Std.DTreeMap.Raw.instSliceableRciSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Rci.Sliceable (Raw α β cmp) α (Internal.RciSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_rci
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Rci.Sliceable.mkSlice t bound...*) = List.filter (fun (e : (a : α) × β a) => (cmp e.fst bound).isGE) t.toList
instance
Std.DTreeMap.Raw.instSliceableRcoSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Rco.Sliceable (Raw α β cmp) α (Internal.RcoSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_rco
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{lowerBound upperBound : α}
:
Slice.toList (Rco.Sliceable.mkSlice t lowerBound...upperBound) = List.filter
(fun (e : (a : α) × β a) => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLT = true))
t.toList
instance
Std.DTreeMap.Raw.instSliceableRccSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Rcc.Sliceable (Raw α β cmp) α (Internal.RccSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_rcc
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{lowerBound upperBound : α}
:
Slice.toList (Rcc.Sliceable.mkSlice t lowerBound...=upperBound) = List.filter
(fun (e : (a : α) × β a) => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLE = true))
t.toList
instance
Std.DTreeMap.Raw.instSliceableRoiSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Roi.Sliceable (Raw α β cmp) α (Internal.RoiSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_roi
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{bound : α}
:
Slice.toList (Roi.Sliceable.mkSlice t bound<...*) = List.filter (fun (e : (a : α) × β a) => (cmp e.fst bound).isGT) t.toList
instance
Std.DTreeMap.Raw.instSliceableRocSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Roc.Sliceable (Raw α β cmp) α (Internal.RocSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_roc
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{lowerBound upperBound : α}
:
Slice.toList (Roc.Sliceable.mkSlice t lowerBound<...=upperBound) = List.filter
(fun (e : (a : α) × β a) => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLE = true))
t.toList
instance
Std.DTreeMap.Raw.instSliceableRooSlice
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
:
Roo.Sliceable (Raw α β cmp) α (Internal.RooSlice α β)
Equations
- One or more equations did not get rendered due to their size.
theorem
Std.DTreeMap.Raw.toList_roo
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
[TransCmp cmp]
{t : Raw α β cmp}
(wf : t.WF)
{lowerBound upperBound : α}
:
Slice.toList (Roo.Sliceable.mkSlice t lowerBound<...upperBound) = List.filter
(fun (e : (a : α) × β a) => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLT = true))
t.toList