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 α β → IterStep (IterM Id ((a : α) × β a)) ((a : α) × β a)

Equations

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

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

Equations

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

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

@[inline]

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

Equations

• Std.DTreeMap.Internal.Zipper.instToIterator = Std.ToIterator.of (Std.DTreeMap.Internal.Zipper α β) fun (z : Std.DTreeMap.Internal.Zipper α β) => z.iter

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 α β → 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.IterStep.done

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

Equations

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

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 α β → 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.IterStep.done

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

Equations

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

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.

@[inline]

instance Std.DTreeMap.Internal.RicSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RicSliceData α β)) Id (RxcIterator α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RicSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RicSliceData α)) Id (Iterators.Types.Map (RxcIterator α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RicSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RicSliceData α β)) Id (Iterators.Types.Map (RxcIterator α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RioSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RioSliceData α β)) Id (RxoIterator α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RioSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RioSliceData α)) Id (Iterators.Types.Map (RxoIterator α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RioSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RioSliceData α β)) Id (Iterators.Types.Map (RxoIterator α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RccSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RccSliceData α β)) Id (RxcIterator α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RccSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RccSliceData α)) Id (Iterators.Types.Map (RxcIterator α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RccSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RccSliceData α β)) Id (Iterators.Types.Map (RxcIterator α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RcoSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RcoSliceData α β)) Id (RxoIterator α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RcoSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RcoSliceData α)) Id (Iterators.Types.Map (RxoIterator α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RcoSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RcoSliceData α β)) Id (Iterators.Types.Map (RxoIterator α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RooSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RooSliceData α β)) Id (RxoIterator α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RooSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RooSliceData α)) Id (Iterators.Types.Map (RxoIterator α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RooSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RooSliceData α β)) Id (Iterators.Types.Map (RxoIterator α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RocSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RocSliceData α β)) Id (RxcIterator α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RocSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RocSliceData α)) Id (Iterators.Types.Map (RxcIterator α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RocSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RocSliceData α β)) Id (Iterators.Types.Map (RxcIterator α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RciSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RciSliceData α β)) Id (Zipper α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RciSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RciSliceData α)) Id (Iterators.Types.Map (Zipper α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RciSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RciSliceData α β)) Id (Iterators.Types.Map (Zipper α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RoiSlice.instToIterator {α : Type u_1} {β : α → Type v} [Ord α] : ToIterator (Slice (RoiSliceData α β)) Id (Zipper α β) ((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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RoiSlice.instToIterator {α : Type u_1} [Ord α] : ToIterator (Slice (RoiSliceData α)) Id (Iterators.Types.Map (Zipper α fun (x : α) => Unit) Id Id (fun ⦃x : Type u_1⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RoiSlice.instToIterator {α : Type u_1} {β : Type v} [Ord α] : ToIterator (Slice (RoiSliceData α β)) Id (Iterators.Types.Map (Zipper α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u_1)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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.

@[inline]

instance Std.DTreeMap.Internal.RiiSlice.instToIterator {α : Type u_1} {β : α → Type v} : ToIterator (Slice (RiiSliceData α β)) Id (Zipper α β) ((a : α) × β a)

Equations

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

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.

@[inline]

instance Std.DTreeMap.Internal.Unit.RiiSlice.instToIterator {α : Type u} : ToIterator (Slice (RiiSliceData α)) Id (Iterators.Types.Map (Zipper α fun (x : α) => Unit) Id Id (fun ⦃x : Type u⦄ => monadLift) fun (b : (_ : α) × Unit) => pure b.fst) α

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.

@[inline]

instance Std.DTreeMap.Internal.Const.RiiSlice.instToIterator {α : Type u} {β : Type v} : ToIterator (Slice (RiiSliceData α β)) Id (Iterators.Types.Map (Zipper α fun (x : α) => β) Id Id (fun ⦃x : Type (max v u)⦄ => monadLift) fun (b : (_ : α) × β) => pure (b.fst, b.snd)) (α × β)

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