source
theorem Std.Iterators.Iter.step_repeat {α : Type w} {f : α → α} {init : α} :
(«repeat» f init).step = PlausibleIterStep.yield («repeat» f (f init)) init ⋯
source
theorem Std.Iterators.Iter.atIdxSlow?_zero_repeat {α : Type w} {f : α → α} {init : α} :
atIdxSlow? 0 («repeat» f init) = some init
source
theorem Std.Iterators.Iter.atIdxSlow?_succ_repeat {α : Type w} {f : α → α} {init : α} {k : Nat} :
atIdxSlow? (k + 1) («repeat» f init) = atIdxSlow? k («repeat» f (f init))
source
theorem Std.Iterators.Iter.atIdxSlow?_succ_repeat_eq_map {α : Type w} {f : α → α} {init : α} {k : Nat} :
atIdxSlow? (k + 1) («repeat» f init) = f <$> atIdxSlow? k («repeat» f init)
source
@[simp]
theorem Std.Iterators.Iter.atIdxSlow?_repeat {α : Type w} {f : α → α} {init : α} {n : Nat} :
atIdxSlow? n («repeat» f init) = some (Nat.repeat f n init)
source
theorem Std.Iterators.Iter.isSome_atIdxSlow?_repeat {α : Type w} {f : α → α} {init : α} {k : Nat} :
(atIdxSlow? k («repeat» f init)).isSome = true
source
@[simp]
theorem Std.Iterators.Iter.toList_take_repeat_succ {α : Type w} {f : α → α} {init : α} {k : Nat} :
(take (k + 1) («repeat» f init)).toList = init :: (take k («repeat» f (f init))).toList