Documentation

Std.Data.Iterators.Lemmas.Combinators.Take

theorem Std.Iterators.Iter.take_eq_toIter_take_toIterM {α β : Type u_1} [Iterator α Id β] {n : Nat} {it : Iter β} :
theorem Std.Iterators.Iter.step_take {α β : Type u_1} [Iterator α Id β] {n : Nat} {it : Iter β} :
(take n it).step = match n with | 0 => PlausibleIterStep.done | k.succ => match it.step with | IterStep.yield it' out, h => PlausibleIterStep.yield (take k it') out | IterStep.skip it', h => PlausibleIterStep.skip (take (k + 1) it') | IterStep.done, h => PlausibleIterStep.done
theorem Std.Iterators.Iter.atIdxSlow?_take {α β : Type u_1} [Iterator α Id β] [Productive α Id] {k l : Nat} {it : Iter β} :
@[simp]
@[simp]
theorem Std.Iterators.Iter.toArray_take_of_finite {α β : Type u_1} [Iterator α Id β] {n : Nat} [Finite α Id] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id] {it : Iter β} :
(take n it).toArray = it.toArray.take n
@[simp]
theorem Std.Iterators.Iter.toList_take_zero {α β : Type u_1} [Iterator α Id β] [Finite (Take α Id β) Id] [IteratorCollect (Take α Id β) Id Id] [LawfulIteratorCollect (Take α Id β) Id Id] {it : Iter β} :
(take 0 it).toList = []