This module provides slice notation for TreeMap slices and implements an iterator
for those slices.
@[simp]
theorem
Std.DTreeMap.Raw.toList_rii
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering := by exact compare)
{t : Raw α β cmp}
:
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
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
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
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
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
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
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
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