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