"No né, já už to dokážu přečíst. To je super."
Tady je k tomu pár funkcí.
def Vector (n : Nat) (α : Type u) := { arr : Array α // arr.size = n }
def Vector.get (v : Vector n α) (i : Fin n) : α :=
v.val.get (v.property.symm i)
def Vector.set (v : Vector n α) (i : Fin n) (x : α) : Vector n α :=
let arr := v.val.set (v.property.symm i) x
let h := v.val.size_set (v.property.symm i) x
⟨arr, v.property h⟩
def Vector.push (v : Vector n α) (x : α) : Vector (n+1) α :=
let arr := v.val.push x
let h := v.val.size_push x
⟨arr, v.property h⟩