@@ -66,7 +66,6 @@ init (x::y::ys) = x :: init (y::ys)
66index : Fin n -> Vect n a -> a
66index : Fin n -> Vect n a -> a
67index FZ (x::xs) = x
67index FZ (x::xs) = x
68index (FS k) (x::xs) = index k xs
68index (FS k) (x::xs) = index k xs
69−index FZ [] impossible
72||| Insert an element at a particular index
71||| Insert an element at a particular index