toArray — Mathlib

English

There is a canonical map from a length-n vector to an array of length n by taking the underlying list elements and converting them to an array.

Русский

Существует каноническая карта от вектора длины n к массиву той же длины: берём элементы подлежащего списка и получаем массив.

LaTeX

$$$\\text{toArray} : \\ Vector\\ α\\ n \\to\\ Array\\ α\\; \\text{ with }\\; toArray(v) = xs.toArray\\text{ where } v = \\langle xs, \\cdot \\rangle$$$

Lean4

/-- Cast a vector to an array. -/
def toArray : Vector α n → Array α
  | ⟨xs, _⟩ => cast (by rfl) xs.toArray

Похожие утверждения