@[inline]

def Std.Iterators.Types.ULiftIterator.modifyStep {α β : Type u} (step : IterStep (Iter β) β) : IterStep (Iter (ULift β)) (ULift β)

Transforms a step of the base iterator into a step of the uLift iterator.

Equations

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

@[inline]

def Std.Iterators.Iter.uLift {α β : Type u} (it : Iter β) : Iter (ULift β)

Transforms an iterator with values in β into one with values in ULift β.

Most other combinators like map cannot switch between universe levels. This combinators makes it possible to transition to a higher universe.

Marble diagram:

it            ---a    ----b    ---c    --d    ---⊥
it.uLift n    ---.up a----.up b---.up c--.up d---⊥

Termination properties:

• Finite: only if the original iterator is finite
• Productive: only if the original iterator is productive

Equations

• it.uLift = (it.toIterM.uLift Id).toIter