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

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

Equations

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

@[simp]

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

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

Equations

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

theorem Std.TreeSet.Raw.toList_ric {α : Type u} (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 bound).isLE) t.toList

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

Equations

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

theorem Std.TreeSet.Raw.toList_rio {α : Type u} (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 bound).isLT) t.toList

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

Equations

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

theorem Std.TreeSet.Raw.toList_rci {α : Type u} (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 bound).isGE) t.toList

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

Equations

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

theorem Std.TreeSet.Raw.toList_rco {α : Type u} (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 lowerBound).isGE = true ∧ (cmp e upperBound).isLT = true)) t.toList

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

Equations

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

theorem Std.TreeSet.Raw.toList_rcc {α : Type u} (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 lowerBound).isGE = true ∧ (cmp e upperBound).isLE = true)) t.toList

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

Equations

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

theorem Std.TreeSet.Raw.toList_roi {α : Type u} (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 bound).isGT) t.toList

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

Equations

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

theorem Std.TreeSet.Raw.toList_roc {α : Type u} (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 lowerBound).isGT = true ∧ (cmp e upperBound).isLE = true)) t.toList

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

Equations

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

theorem Std.TreeSet.Raw.toList_roo {α : Type u} (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 lowerBound).isGT = true ∧ (cmp e upperBound).isLT = true)) t.toList