English
The operation insertIdx inserts an element a into a vector v at position i ∈ Fin(n+1), producing a new vector of length n+1 whose underlying list has a inserted at index i.
Русский
Операция insertIdx вставляет элемент a в вектор v на позиции i ∈ Fin(n+1), получая новый вектор длины n+1 с элементом a, вставленным на месте i.
LaTeX
$$$\\text{insertIdx}\\; (a)\\; (i)\\; (v) : \\ Vector\\ α\\ (n+1) \\\\text{ с } (v).val.insertIdx i.1 a$$$
Lean4
/-- `v.insertIdx a i` inserts `a` into the vector `v` at position `i`
(and shifting later components to the right). -/
def insertIdx (a : α) (i : Fin (n + 1)) (v : Vector α n) : Vector α (n + 1) :=
⟨v.1.insertIdx i a, by
rw [List.length_insertIdx, v.2]
split <;> omega⟩
