inductive Std.DTreeMap.Internal.Zipper (α : Type u) (β : α → Type v) : Type (max u v)

• done {α : Type u} {β : α → Type v} : Zipper α β
• cons {α : Type u} {β : α → Type v} (k : α) (v : β k) (tree : Impl α β) (next : Zipper α β) : Zipper α β

def Std.DTreeMap.Internal.Zipper.toList {α : Type u} {β : α → Type v} : Zipper α β → List ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.Zipper.done.toList = []
• (Std.DTreeMap.Internal.Zipper.cons k v tree next).toList = ⟨k, v⟩ :: tree.toList ++ next.toList

def Std.DTreeMap.Internal.Zipper.Ordered {α : Type u} {β : α → Type v} [Ord α] (t : Zipper α β) : Prop

Equations

• t.Ordered = List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) t.toList

def Std.DTreeMap.Internal.Zipper.prependMap {α : Type u} {β : α → Type v} : Impl α β → Zipper α β → Zipper α β

Equations

• Std.DTreeMap.Internal.Zipper.prependMap Std.DTreeMap.Internal.Impl.leaf x✝ = x✝
• Std.DTreeMap.Internal.Zipper.prependMap (Std.DTreeMap.Internal.Impl.inner size k v l r) x✝ = Std.DTreeMap.Internal.Zipper.prependMap l (Std.DTreeMap.Internal.Zipper.cons k v r x✝)

def Std.DTreeMap.Internal.Zipper.prependMapGE {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (lowerBound : α) (it : Zipper α β) : Zipper α β

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Zipper.prependMapGE Std.DTreeMap.Internal.Impl.leaf lowerBound it = it

def Std.DTreeMap.Internal.Zipper.prependMapGT {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (lowerBound : α) (it : Zipper α β) : Zipper α β

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Zipper.prependMapGT Std.DTreeMap.Internal.Impl.leaf lowerBound it = it

def Std.DTreeMap.Internal.Zipper.step {α : Type u} {β : α → Type v} : Zipper α β → Iterators.IterStep (IterM Id ((a : α) × β a)) ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.Zipper.done.step = Std.Iterators.IterStep.done
• (Std.DTreeMap.Internal.Zipper.cons k v tree next).step = Std.Iterators.IterStep.yield { internalState := Std.DTreeMap.Internal.Zipper.prependMap tree next } ⟨k, v⟩

instance Std.DTreeMap.Internal.instIteratorZipperIdSigma {α : Type u} {β : α → Type v} : Iterators.Iterator (Zipper α β) Id ((a : α) × β a)

Equations

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

instance Std.DTreeMap.Internal.instIteratorCollectZipperIdSigma {α : Type u} {β : α → Type v} : Iterators.IteratorCollect (Zipper α β) Id Id

Equations

• Std.DTreeMap.Internal.instIteratorCollectZipperIdSigma = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.DTreeMap.Internal.Zipper.instFinite {α : Type u} {β : α → Type v} : Iterators.Finite (Zipper α β) Id

def Std.DTreeMap.Internal.Zipper.iter {α : Type u} {β : α → Type v} (t : Zipper α β) : Iter ((a : α) × β a)

Equations

• t.iter = { internalState := t }

def Std.DTreeMap.Internal.Zipper.iterOfTree {α : Type u} {β : α → Type v} (t : Impl α β) : Iter ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.Zipper.iterOfTree t = (Std.DTreeMap.Internal.Zipper.prependMap t Std.DTreeMap.Internal.Zipper.done).iter

instance Std.DTreeMap.Internal.instToIteratorZipperIdSigma {α : Type u} {β : α → Type v} {z : Zipper α β} : Iterators.ToIterator z Id ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.instToIteratorZipperIdSigma = { State := Std.DTreeMap.Internal.Zipper α β, iterMInternal := z.iter.toIterM }

theorem Std.DTreeMap.Internal.Zipper.toList_iterOfTree {α : Type u} {β : α → Type v} (t : Impl α β) : (iterOfTree t).toList = t.toList

structure Std.DTreeMap.Internal.RxcIterator (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• iter : Zipper α β
• upper : α

def Std.DTreeMap.Internal.RxcIterator.step {α : Type u} {β : α → Type v} [Ord α] : RxcIterator α β → Iterators.IterStep (IterM Id ((a : α) × β a)) ((a : α) × β a)

Equations

• One or more equations did not get rendered due to their size.
• { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }.step = Std.Iterators.IterStep.done

instance Std.DTreeMap.Internal.instIteratorRxcIteratorIdSigma {α : Type u} {β : α → Type v} [Ord α] : Iterators.Iterator (RxcIterator α β) Id ((a : α) × β a)

Equations

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

instance Std.DTreeMap.Internal.instIteratorCollectRxcIteratorIdSigma {α : Type u} {β : α → Type v} [Ord α] : Iterators.IteratorCollect (RxcIterator α β) Id Id

Equations

• Std.DTreeMap.Internal.instIteratorCollectRxcIteratorIdSigma = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.DTreeMap.Internal.instFinite {α : Type u} {β : α → Type v} [Ord α] : Iterators.Finite (RxcIterator α β) Id

theorem Std.DTreeMap.Internal.RxcIterator.takeWhile_toList {α : Type u_1} {β : α → Type u_2} [Ord α] [TransOrd α] {z : Zipper α β} {bound : α} {z_ord : z.Ordered} : List.takeWhile (fun (e : (a : α) × β a) => (compare e.fst bound).isLE) z.toList = List.filter (fun (e : (a : α) × β a) => (compare e.fst bound).isLE) z.toList

structure Std.DTreeMap.Internal.RxoIterator (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• iter : Zipper α β
• upper : α

def Std.DTreeMap.Internal.RxoIterator.step {α : Type u} {β : α → Type v} [Ord α] : RxoIterator α β → Iterators.IterStep (IterM Id ((a : α) × β a)) ((a : α) × β a)

Equations

• One or more equations did not get rendered due to their size.
• { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }.step = Std.Iterators.IterStep.done

instance Std.DTreeMap.Internal.instIteratorRxoIteratorIdSigma {α : Type u} {β : α → Type v} [Ord α] : Iterators.Iterator (RxoIterator α β) Id ((a : α) × β a)

Equations

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

instance Std.DTreeMap.Internal.instIteratorCollectRxoIteratorIdSigma {α : Type u} {β : α → Type v} [Ord α] : Iterators.IteratorCollect (RxoIterator α β) Id Id

Equations

• Std.DTreeMap.Internal.instIteratorCollectRxoIteratorIdSigma = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.DTreeMap.Internal.Rxo.instFinite {α : Type u} {β : α → Type v} [Ord α] : Iterators.Finite (RxoIterator α β) Id

theorem Std.DTreeMap.Internal.RxoIterator.takeWhile_toList {α : Type u_1} {β : α → Type u_2} [Ord α] [TransOrd α] {z : Zipper α β} {bound : α} {z_ord : z.Ordered} : List.takeWhile (fun (e : (a : α) × β a) => (compare e.fst bound).isLT) z.toList = List.filter (fun (e : (a : α) × β a) => (compare e.fst bound).isLT) z.toList

structure Std.DTreeMap.Internal.RicSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Ric α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RicSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RicSlice α β = Std.Slice (Std.DTreeMap.Internal.RicSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRicSlice {α : Type u} {β : α → Type v} [Ord α] : Ric.Sliceable (Impl α β) α (RicSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRicSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RicSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_ric {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (bound : α) : Slice.toList (Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun (e : (a : α) × β a) => (compare e.fst bound).isLE) t.toList

structure Std.DTreeMap.Internal.Unit.RicSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Ric α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RicSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RicSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RicSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRicSlice {α : Type u} [Ord α] : Ric.Sliceable (Impl α fun (x : α) => Unit) α (RicSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRicSliceId {α : Type u_1} [Ord α] {s : RicSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_ric {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (bound : α) : Slice.toList (Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun (e : α) => (compare e bound).isLE) t.keys

structure Std.DTreeMap.Internal.Const.RicSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Ric α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RicSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RicSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RicSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRicSlice {α : Type u} {β : Type v} [Ord α] : Ric.Sliceable (Impl α fun (x : α) => β) α (RicSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRicSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RicSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_ric {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (bound : α) : Slice.toList (Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun (e : α × β) => (compare e.fst bound).isLE) (Impl.Const.toList t)

structure Std.DTreeMap.Internal.RioSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Rio α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RioSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RioSlice α β = Std.Slice (Std.DTreeMap.Internal.RioSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRioSlice {α : Type u} {β : α → Type v} [Ord α] : Rio.Sliceable (Impl α β) α (RioSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRioSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RioSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_rio {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (bound : α) : Slice.toList (Rio.Sliceable.mkSlice t *...bound) = List.filter (fun (e : (a : α) × β a) => (compare e.fst bound).isLT) t.toList

structure Std.DTreeMap.Internal.Unit.RioSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Rio α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RioSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RioSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RioSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRioSlice {α : Type u} [Ord α] : Rio.Sliceable (Impl α fun (x : α) => Unit) α (RioSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRioSliceId {α : Type u_1} [Ord α] {s : RioSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_rio {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (bound : α) : Slice.toList (Rio.Sliceable.mkSlice t *...bound) = List.filter (fun (e : α) => (compare e bound).isLT) t.keys

structure Std.DTreeMap.Internal.Const.RioSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Rio α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RioSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RioSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RioSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRioSlice {α : Type u} {β : Type v} [Ord α] : Rio.Sliceable (Impl α fun (x : α) => β) α (RioSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRioSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RioSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_rio {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (bound : α) : Slice.toList (Rio.Sliceable.mkSlice t *...bound) = List.filter (fun (e : α × β) => (compare e.fst bound).isLT) (Impl.Const.toList t)

@[always_inline]

def Std.DTreeMap.Internal.rccIterator {α : Type u_1} {β : α → Type u_2} [Ord α] (t : Impl α β) (lowerBound upperBound : α) : Iter ((a : α) × β a)

Equations

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

structure Std.DTreeMap.Internal.RccSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Rcc α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RccSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RccSlice α β = Std.Slice (Std.DTreeMap.Internal.RccSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRccSlice {α : Type u} {β : α → Type v} [Ord α] : Rcc.Sliceable (Impl α β) α (RccSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRccSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RccSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_rcc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Rcc.Sliceable.mkSlice t lowerBound...=upperBound) = List.filter (fun (e : (a : α) × β a) => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLE = true)) t.toList

structure Std.DTreeMap.Internal.Unit.RccSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Rcc α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RccSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RccSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RccSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRccSlice {α : Type u} [Ord α] : Rcc.Sliceable (Impl α fun (x : α) => Unit) α (RccSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRccSliceId {α : Type u_1} [Ord α] {s : RccSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_rcc {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Rcc.Sliceable.mkSlice t lowerBound...=upperBound) = List.filter (fun (e : α) => decide ((compare e lowerBound).isGE = true ∧ (compare e upperBound).isLE = true)) t.keys

structure Std.DTreeMap.Internal.Const.RccSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Rcc α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RccSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RccSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RccSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRccSlice {α : Type u} {β : Type v} [Ord α] : Rcc.Sliceable (Impl α fun (x : α) => β) α (RccSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRccSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RccSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_rcc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Rcc.Sliceable.mkSlice t lowerBound...=upperBound) = List.filter (fun (e : α × β) => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLE = true)) (Impl.Const.toList t)

@[always_inline]

def Std.DTreeMap.Internal.rcoIterator {α : Type u_1} {β : α → Type u_2} [Ord α] (t : Impl α β) (lowerBound upperBound : α) : Iter ((a : α) × β a)

Equations

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

structure Std.DTreeMap.Internal.RcoSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Rco α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RcoSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RcoSlice α β = Std.Slice (Std.DTreeMap.Internal.RcoSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRcoSlice {α : Type u} {β : α → Type v} [Ord α] : Rco.Sliceable (Impl α β) α (RcoSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRcoSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RcoSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_rco {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Rco.Sliceable.mkSlice t lowerBound...upperBound) = List.filter (fun (e : (a : α) × β a) => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLT = true)) t.toList

structure Std.DTreeMap.Internal.Unit.RcoSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Rco α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RcoSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RcoSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RcoSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRcoSlice {α : Type u} [Ord α] : Rco.Sliceable (Impl α fun (x : α) => Unit) α (RcoSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRcoSliceId {α : Type u_1} [Ord α] {s : RcoSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_rco {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Rco.Sliceable.mkSlice t lowerBound...upperBound) = List.filter (fun (e : α) => decide ((compare e lowerBound).isGE = true ∧ (compare e upperBound).isLT = true)) t.keys

structure Std.DTreeMap.Internal.Const.RcoSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Rco α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RcoSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RcoSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RcoSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRcoSlice {α : Type u} {β : Type v} [Ord α] : Rco.Sliceable (Impl α fun (x : α) => β) α (RcoSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRcoSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RcoSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_rco {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Rco.Sliceable.mkSlice t lowerBound...upperBound) = List.filter (fun (e : α × β) => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLT = true)) (Impl.Const.toList t)

@[always_inline]

def Std.DTreeMap.Internal.rooIterator {α : Type u_1} {β : α → Type u_2} [Ord α] (t : Impl α β) (lowerBound upperBound : α) : Iter ((a : α) × β a)

Equations

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

structure Std.DTreeMap.Internal.RooSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Roo α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RooSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RooSlice α β = Std.Slice (Std.DTreeMap.Internal.RooSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRooSlice {α : Type u} {β : α → Type v} [Ord α] : Roo.Sliceable (Impl α β) α (RooSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRooSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RooSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_roo {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Roo.Sliceable.mkSlice t lowerBound<...upperBound) = List.filter (fun (e : (a : α) × β a) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLT = true)) t.toList

structure Std.DTreeMap.Internal.Unit.RooSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Roo α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RooSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RooSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RooSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRooSlice {α : Type u} [Ord α] : Roo.Sliceable (Impl α fun (x : α) => Unit) α (RooSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRooSliceId {α : Type u_1} [Ord α] {s : RooSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_roo {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Roo.Sliceable.mkSlice t lowerBound<...upperBound) = List.filter (fun (e : α) => decide ((compare e lowerBound).isGT = true ∧ (compare e upperBound).isLT = true)) t.keys

structure Std.DTreeMap.Internal.Const.RooSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Roo α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RooSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RooSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RooSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRooSlice {α : Type u} {β : Type v} [Ord α] : Roo.Sliceable (Impl α fun (x : α) => β) α (RooSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRooSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RooSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_roo {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Roo.Sliceable.mkSlice t lowerBound<...upperBound) = List.filter (fun (e : α × β) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLT = true)) (Impl.Const.toList t)

@[always_inline]

def Std.DTreeMap.Internal.rocIterator {α : Type u_1} {β : α → Type u_2} [Ord α] (t : Impl α β) (lowerBound upperBound : α) : Iter ((a : α) × β a)

Equations

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

structure Std.DTreeMap.Internal.RocSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Roc α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RocSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RocSlice α β = Std.Slice (Std.DTreeMap.Internal.RocSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRocSlice {α : Type u} {β : α → Type v} [Ord α] : Roc.Sliceable (Impl α β) α (RocSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRocSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RocSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_roc {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Roc.Sliceable.mkSlice t lowerBound<...=upperBound) = List.filter (fun (e : (a : α) × β a) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLE = true)) t.toList

structure Std.DTreeMap.Internal.Unit.RocSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Roc α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RocSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RocSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RocSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRocSlice {α : Type u} [Ord α] : Roc.Sliceable (Impl α fun (x : α) => Unit) α (RocSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRocSliceId {α : Type u_1} [Ord α] {s : RocSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_roc {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Roc.Sliceable.mkSlice t lowerBound<...=upperBound) = List.filter (fun (e : α) => decide ((compare e lowerBound).isGT = true ∧ (compare e upperBound).isLE = true)) t.keys

structure Std.DTreeMap.Internal.Const.RocSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Roc α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RocSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RocSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RocSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRocSlice {α : Type u} {β : Type v} [Ord α] : Roc.Sliceable (Impl α fun (x : α) => β) α (RocSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRocSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RocSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_roc {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (lowerBound upperBound : α) : Slice.toList (Roc.Sliceable.mkSlice t lowerBound<...=upperBound) = List.filter (fun (e : α × β) => decide ((compare e.fst lowerBound).isGT = true ∧ (compare e.fst upperBound).isLE = true)) (Impl.Const.toList t)

@[always_inline]

def Std.DTreeMap.Internal.rciIterator {α : Type u_1} {β : α → Type u_2} [Ord α] (t : Impl α β) (lowerBound : α) : Iter ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.rciIterator t lowerBound = { internalState := Std.DTreeMap.Internal.Zipper.prependMapGE t lowerBound Std.DTreeMap.Internal.Zipper.done }

structure Std.DTreeMap.Internal.RciSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Rci α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RciSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RciSlice α β = Std.Slice (Std.DTreeMap.Internal.RciSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRciSlice {α : Type u} {β : α → Type v} [Ord α] : Rci.Sliceable (Impl α β) α (RciSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRciSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RciSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_rci {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound : α) : Slice.toList (Rci.Sliceable.mkSlice t lowerBound...*) = List.filter (fun (e : (a : α) × β a) => (compare e.fst lowerBound).isGE) t.toList

structure Std.DTreeMap.Internal.Unit.RciSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Rci α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RciSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RciSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RciSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRciSlice {α : Type u} [Ord α] : Rci.Sliceable (Impl α fun (x : α) => Unit) α (RciSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRciSliceId {α : Type u_1} [Ord α] {s : RciSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_rci {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (lowerBound : α) : Slice.toList (Rci.Sliceable.mkSlice t lowerBound...*) = List.filter (fun (e : α) => (compare e lowerBound).isGE) t.keys

structure Std.DTreeMap.Internal.Const.RciSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Rci α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RciSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RciSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RciSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRciSlice {α : Type u} {β : Type v} [Ord α] : Rci.Sliceable (Impl α fun (x : α) => β) α (RciSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRciSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RciSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_rci {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (lowerBound : α) : Slice.toList (Rci.Sliceable.mkSlice t lowerBound...*) = List.filter (fun (e : α × β) => (compare e.fst lowerBound).isGE) (Impl.Const.toList t)

@[always_inline]

def Std.DTreeMap.Internal.roiIterator {α : Type u_1} {β : α → Type u_2} [Ord α] (t : Impl α β) (lowerBound : α) : Iter ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.roiIterator t lowerBound = { internalState := Std.DTreeMap.Internal.Zipper.prependMapGT t lowerBound Std.DTreeMap.Internal.Zipper.done }

structure Std.DTreeMap.Internal.RoiSliceData (α : Type u) (β : α → Type v) [Ord α] : Type (max u v)

• treeMap : Impl α β
• range : Roi α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RoiSlice (α : Type u_1) (β : α → Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RoiSlice α β = Std.Slice (Std.DTreeMap.Internal.RoiSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRoiSlice {α : Type u} {β : α → Type v} [Ord α] : Roi.Sliceable (Impl α β) α (RoiSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRoiSliceIdSigma {α : Type u_1} {β : α → Type u_2} [Ord α] {s : RoiSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

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

theorem Std.DTreeMap.Internal.toList_roi {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (t : Impl α β) (ordered : t.Ordered) (lowerBound : α) : Slice.toList (Roi.Sliceable.mkSlice t lowerBound<...*) = List.filter (fun (e : (a : α) × β a) => (compare e.fst lowerBound).isGT) t.toList

structure Std.DTreeMap.Internal.Unit.RoiSliceData (α : Type u) [Ord α] : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Roi α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RoiSlice (α : Type u_1) [Ord α] : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RoiSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RoiSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRoiSlice {α : Type u} [Ord α] : Roi.Sliceable (Impl α fun (x : α) => Unit) α (RoiSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRoiSliceId {α : Type u_1} [Ord α] {s : RoiSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_roi {α : Type u} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => Unit) (ordered : t.Ordered) (lowerBound : α) : Slice.toList (Roi.Sliceable.mkSlice t lowerBound<...*) = List.filter (fun (e : α) => (compare e lowerBound).isGT) t.keys

structure Std.DTreeMap.Internal.Const.RoiSliceData (α : Type u) (β : Type v) [Ord α] : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Roi α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RoiSlice (α : Type u_1) (β : Type u_2) [Ord α] : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RoiSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RoiSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRoiSlice {α : Type u} {β : Type v} [Ord α] : Roi.Sliceable (Impl α fun (x : α) => β) α (RoiSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRoiSliceIdProd {α : Type u_1} {β : Type u_2} [Ord α] {s : RoiSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_roi {α : Type u} {β : Type v} [Ord α] [TransOrd α] (t : Impl α fun (x : α) => β) (ordered : t.Ordered) (lowerBound : α) : Slice.toList (Roi.Sliceable.mkSlice t lowerBound<...*) = List.filter (fun (e : α × β) => (compare e.fst lowerBound).isGT) (Impl.Const.toList t)

def Std.DTreeMap.Internal.riiIterator {α : Type u_1} {β : α → Type u_2} (t : Impl α β) : Iter ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.riiIterator t = { internalState := Std.DTreeMap.Internal.Zipper.prependMap t Std.DTreeMap.Internal.Zipper.done }

structure Std.DTreeMap.Internal.RiiSliceData (α : Type u) (β : α → Type v) : Type (max u v)

• treeMap : Impl α β
• range : Rii α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.RiiSlice (α : Type u_1) (β : α → Type u_2) : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.RiiSlice α β = Std.Slice (Std.DTreeMap.Internal.RiiSliceData α β)

instance Std.DTreeMap.Internal.instSliceableImplRiiSlice {α : Type u} {β : α → Type v} : Rii.Sliceable (Impl α β) α (RiiSlice α β)

Equations

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

instance Std.DTreeMap.Internal.instToIteratorRiiSliceIdSigma {α : Type u_1} {β : α → Type u_2} {s : RiiSlice α β} : Iterators.ToIterator s Id ((a : α) × β a)

Equations

• Std.DTreeMap.Internal.instToIteratorRiiSliceIdSigma = Std.Iterators.ToIterator.of (Std.DTreeMap.Internal.Zipper α β) (Std.DTreeMap.Internal.riiIterator s.internalRepresentation.treeMap)

theorem Std.DTreeMap.Internal.toList_rii {α : Type u} {β : α → Type v} (t : Impl α β) : Slice.toList (Rii.Sliceable.mkSlice t *...*) = t.toList

structure Std.DTreeMap.Internal.Unit.RiiSliceData (α : Type u) : Type u

• treeMap : Impl α fun (x : α) => Unit
• range : Rii α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Unit.RiiSlice (α : Type u_1) : Type u_1

Equations

• Std.DTreeMap.Internal.Unit.RiiSlice α = Std.Slice (Std.DTreeMap.Internal.Unit.RiiSliceData α)

instance Std.DTreeMap.Internal.Unit.instSliceableImplUnitRiiSlice {α : Type u} : Rii.Sliceable (Impl α fun (x : α) => Unit) α (RiiSlice α)

Equations

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

instance Std.DTreeMap.Internal.Unit.instToIteratorRiiSliceId {α : Type u_1} {s : RiiSlice α} : Iterators.ToIterator s Id α

Equations

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

theorem Std.DTreeMap.Internal.Unit.toList_rii {α : Type u} (t : Impl α fun (x : α) => Unit) : Slice.toList (Rii.Sliceable.mkSlice t *...*) = t.keys

structure Std.DTreeMap.Internal.Const.RiiSliceData (α : Type u) (β : Type v) : Type (max u v)

• treeMap : Impl α fun (x : α) => β
• range : Rii α

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Const.RiiSlice (α : Type u_1) (β : Type u_2) : Type (max u_2 u_1)

Equations

• Std.DTreeMap.Internal.Const.RiiSlice α β = Std.Slice (Std.DTreeMap.Internal.Const.RiiSliceData α β)

instance Std.DTreeMap.Internal.Const.instSliceableImplRiiSlice {α : Type u} {β : Type v} : Rii.Sliceable (Impl α fun (x : α) => β) α (RiiSlice α β)

Equations

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

instance Std.DTreeMap.Internal.Const.instToIteratorRiiSliceIdProd {α : Type u_1} {β : Type u_2} {s : RiiSlice α β} : Iterators.ToIterator s Id (α × β)

Equations

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

theorem Std.DTreeMap.Internal.Const.toList_rii {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) : Slice.toList (Rii.Sliceable.mkSlice t *...*) = Impl.Const.toList t