English
There is a function scanl that produces a Vector β (n+1) from a Vector α n by performing a left-to-right scan using f and starting value b.
Русский
Существует функция scanl, которая даёт вектор β (n+1) из вектора α n путём слева направо с применением f и начального значения b.
LaTeX
$$$\\mathrm{scanl} : \\mathrm{Vector}\\ \\beta\\ (n+1)\\;:=\\;\\langle \\mathrm{List.scanl}(f,b,v.toList),\\; \\text{length proof}\\rangle$$$
Lean4
/-- Construct a `Vector β (n + 1)` from a `Vector α n` by scanning `f : β → α → β`
from the "left", that is, from 0 to `Fin.last n`, using `b : β` as the starting value.
-/
def scanl : Vector β (n + 1) :=
⟨List.scanl f b v.toList, by rw [List.length_scanl, toList_length]⟩
