snoc — Mathlib

English

snoc extends a vector by appending a single element: (xs) snoc x = xs ++ x ::ᵥ Vector.nil.

Русский

snoc добавляет один элемент в конец вектора: (xs) snoc x = xs ++ x ::ᵥ Vector.nil.

LaTeX

$$$\text{snoc} : Vector\ α\ n \to α \to Vector\ α\ (n+1)\quad(\text{snoc } xs\ x = xs \ ++\ x ::ᵥ\ Vector.nil)$$$

Lean4

/-- Append a single element to the end of a vector -/
def snoc : Vector α n → α → Vector α (n + 1) := fun xs x => xs ++ x ::ᵥ Vector.nil

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