Documentation

Std.Data.Iterators.Lemmas.Combinators.TakeWhile

theorem Std.Iterators.Iter.takeWhile_eq {α β : Type u_1} [Iterator α Id β] {P : βBool} {it : Iter β} :
theorem Std.Iterators.Iter.step_takeWhile {α β : Type u_1} [Iterator α Id β] {P : βBool} {it : Iter β} :
(takeWhile P it).step = match it.step with | IterStep.yield it' out, h => match P out with | true => PlausibleIterStep.yield (takeWhile P it') out | false => PlausibleIterStep.done | IterStep.skip it', h => PlausibleIterStep.skip (takeWhile P it') | IterStep.done, h => PlausibleIterStep.done
theorem Std.Iterators.Iter.atIdxSlow?_takeWhile {α β : Type u_1} [Iterator α Id β] [Productive α Id] {l : Nat} {it : Iter β} {P : βBool} :
atIdxSlow? l (takeWhile P it) = if ∀ (k : Nat), k lOption.any P (atIdxSlow? k it) = true then atIdxSlow? l it else none