theorem Std.IterM.step_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad n] {it : IterM m β} [MonadLiftT m (Iterators.ULiftT n)] : (it.uLift n).step = do let __do_lift ← (monadLift it.step).run match __do_lift.down.inflate with | ⟨IterStep.yield it' out, h⟩ => pure (Shrink.deflate (PlausibleIterStep.yield (it'.uLift n) { down := out } ⋯)) | ⟨IterStep.skip it', h⟩ => pure (Shrink.deflate (PlausibleIterStep.skip (it'.uLift n) ⋯)) | ⟨IterStep.done, h⟩ => pure (Shrink.deflate (PlausibleIterStep.done ⋯))

@[simp]

theorem Std.IterM.toList_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (Iterators.ULiftT n)] [Iterators.Finite α m] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m (Iterators.ULiftT n)] : (it.uLift n).toList = (fun (l : ULift (List β)) => List.map ULift.up l.down) <$> (monadLift it.toList).run

@[simp]

theorem Std.IterM.toListRev_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (Iterators.ULiftT n)] [Iterators.Finite α m] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m (Iterators.ULiftT n)] : (it.uLift n).toListRev = (fun (l : ULift (List β)) => List.map ULift.up l.down) <$> (monadLift it.toListRev).run

@[simp]

theorem Std.IterM.toArray_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (Iterators.ULiftT n)] [Iterators.Finite α m] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m (Iterators.ULiftT n)] : (it.uLift n).toArray = (fun (l : ULift (Array β)) => Array.map ULift.up l.down) <$> (monadLift it.toArray).run

@[simp]

theorem Std.IterM.length_uLift {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (Iterators.ULiftT n)] [Iterators.Finite α m] [IteratorLoop α m m] [LawfulMonad m] [LawfulMonad n] [LawfulIteratorLoop α m m] [LawfulMonadLiftT m (Iterators.ULiftT n)] : (it.uLift n).length = (fun (x : ULift (ULift Nat)) => { down := x.down.down }) <$> (monadLift it.length).run

@[deprecated Std.IterM.length_uLift (since := "2026-01-28")]

def Std.IterM.count_uLift {α : Type u_1} {m : Type u_1 → Type u_2} {n : Type (max u_1 u_3) → Type u_4} {β : Type u_1} [Iterator α m β] [Monad m] [Monad n] {it : IterM m β} [MonadLiftT m (Iterators.ULiftT n)] [Iterators.Finite α m] [IteratorLoop α m m] [LawfulMonad m] [LawfulMonad n] [LawfulIteratorLoop α m m] [LawfulMonadLiftT m (Iterators.ULiftT n)] : (it.uLift n).length = (fun (x : ULift (ULift Nat)) => { down := x.down.down }) <$> (monadLift it.length).run

Equations

• @Std.IterM.count_uLift = @Std.IterM.length_uLift