This module provides slice notation for TreeMap slices and implements an iterator for those slices.

instance Std.TreeMap.Raw.instSliceableRiiSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Rii.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RiiSlice α β)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.TreeMap.Raw.toList_rii {α : Type ąu} {β : Type v} (cmp : α → α → Ordering := by exact compare) {t : Raw α β cmp} : Slice.toList (Rii.Sliceable.mkSlice t *...*) = t.toList

instance Std.TreeMap.Raw.instSliceableRicSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Ric.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RicSlice α β)

Equations

• One or more equations did not get rendered due to their size.

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

instance Std.TreeMap.Raw.instSliceableRioSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Rio.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RioSlice α β)

Equations

• One or more equations did not get rendered due to their size.

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

instance Std.TreeMap.Raw.instSliceableRciSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Rci.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RciSlice α β)

Equations

• One or more equations did not get rendered due to their size.

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

instance Std.TreeMap.Raw.instSliceableRcoSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Rco.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RcoSlice α β)

Equations

• One or more equations did not get rendered due to their size.

theorem Std.TreeMap.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 : α × β) => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLT = true)) t.toList

instance Std.TreeMap.Raw.instSliceableRccSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Rcc.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RccSlice α β)

Equations

• One or more equations did not get rendered due to their size.

theorem Std.TreeMap.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 : α × β) => decide ((cmp e.fst lowerBound).isGE = true ∧ (cmp e.fst upperBound).isLE = true)) t.toList

instance Std.TreeMap.Raw.instSliceableRoiSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Roi.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RoiSlice α β)

Equations

• One or more equations did not get rendered due to their size.

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

instance Std.TreeMap.Raw.instSliceableRocSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Roc.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RocSlice α β)

Equations

• One or more equations did not get rendered due to their size.

theorem Std.TreeMap.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 : α × β) => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLE = true)) t.toList

instance Std.TreeMap.Raw.instSliceableRooSlice {α : Type u} {β : Type v} (cmp : α → α → Ordering := by exact compare) : Roo.Sliceable (Raw α β cmp) α (DTreeMap.Internal.Const.RooSlice α β)

Equations

• One or more equations did not get rendered due to their size.

theorem Std.TreeMap.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 : α × β) => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLT = true)) t.toList