Remove a no longer necessary `impossible`
commitf46f57aaf81e65d65b429728fbf2795da6260e69
authorMelvar Chen <Melvar.Chen@googlemail.com>
dateThu 13 Nov 2014, 17:29 (12 years ago)
parentefd6f8a
libs/prelude/Prelude/Vect.idr−1
@@ -66,7 +66,6 @@ init (x::y::ys) = x :: init (y::ys)
6666index : Fin n -> Vect n a -> a
6767index FZ (x::xs) = x
6868index (FS k) (x::xs) = index k xs
69−index FZ [] impossible
7069
7170
7271||| Insert an element at a particular index