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