English
snoc appends an element at the end of an n-tuple, giving a function on Fin(n+1) by either using the tail value transformed from p or the new last element x, with appropriate casting.
Русский
snoc добавляет элемент в конец (n)-кортежа, образуя функцию на Fin(n+1): либо применяется преобразованный хвостовый элемент p, либо новый последний элемент x, с необходимым приведом типов.
LaTeX
$$$\\mathrm{snoc}\\ p\\ x : Fin(n+1) \\to α\\ (\n\\text{определение по }\ \text{if } i.\\text{val} < n \\text{ тогда } \\mathrm{cast}\\ (p (\\mathrm{castLT}\\ i\\ h)) \\ else \\mathrm{cast}\\ (\\text{eq_last_of_not_lt}\\ h)\\ x$$$
Lean4
/-- Adding an element at the end of an `n`-tuple, to get an `n+1`-tuple. The name `snoc` comes from
`cons` (i.e., adding an element to the left of a tuple) read in reverse order. -/
def snoc (p : ∀ i : Fin n, α i.castSucc) (x : α (last n)) (i : Fin (n + 1)) : α i :=
if h : i.val < n then _root_.cast (by rw [Fin.castSucc_castLT i h]) (p (castLT i h))
else _root_.cast (by rw [eq_last_of_not_lt h]) x
