append1 — Mathlib

English

append1 extends a TypeVec by one element: (append1 α β)(Fin2.fs i) = α i and (append1 α β)(Fin2.fz) = β.

Русский

append1 расширяет TypeVec на один элемент: (append1 α β)(Fin2.fs i) = α i и (append1 α β)(Fin2.fz) = β.

LaTeX

$${n : Nat} → {α : TypeVec n} → {β : Type*} → TypeVec (n + 1) :=\n α|Fin2.fs i → α i; β for Fin2.fz$$

Lean4

/-- Support for extending a `TypeVec` by one element. -/
def append1 (α : TypeVec n) (β : Type*) : TypeVec (n + 1)
  | Fin2.fs i => α i
  | Fin2.fz => β

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