Merge pull request #1712 from Melvar/remove-impossible
Remove a no longer necessary `impossible`
commite452845709bb128de5360e46783ad114771a5440
authorEdwin Brady <edwin.brady@gmail.com>
dateThu 4 Dec 2014, 19:16 (12 years ago)
parent7afa03af46f57a
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