Theorems · Definition · combinatorics

List.Vector.scanl

{α : Type u_1} → {n : ℕ} → {β : Type u_6} → (β → α → β) → β → List.Vector α n → List.Vector β (n + 1)

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.

Defined in

Mathlib.Data.Vector.Basic

Cited by

7 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound