Theorems · Theorem · combinatorics

List.Vector.scanl_singleton

∀ {α : Type u_1} {β : Type u_6} (f : β → α → β) (b : β) (v : List.Vector α 1),
  List.Vector.scanl f b v = b ::ᵥ f b v.head ::ᵥ List.Vector.nil

The recursive step of scanl splits a vector made up of a single element x ::ᵥ nil : Vector α 1 into a Vector of the provided starting value b : β and the mapped f b x : β as the last value.

Defined in

Mathlib.Data.Vector.Basic

Cited by

1 results in Mathlib

Foundations

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