@@ -161,8 +161,7 @@ init' [] = Nothing
161161init' (x::xs) =
162162 case xs of
163163 [] => Just []
164− y::ys =>
165− -- XXX: Problem with typechecking a "do" block here
164+ y::ys =>
166165 case init' $ y::ys of
167166 Nothing => Nothing
168167 Just j => Just $ x :: j
@@ -274,42 +273,38 @@ instance Functor List where
274273-- Zips and unzips
275274--------------------------------------------------------------------------------
276275
277−||| Combine two lists of the same length elementwise using some function.
276+||| Combine two lists elementwise using some function. If they are different
277+||| lengths, the result is truncated to the length of the shorter list.
278278||| @ f the function to combine elements with
279279||| @ l the first list
280280||| @ r the second list
281−||| @ ok a proof that the lengths of the inputs are equal
282−zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) ->
283− (ok : length l = length r) -> List c
284−zipWith f [] (y::ys) Refl impossible
285−zipWith f (x::xs) [] Refl impossible
286−zipWith f [] [] p = []
287−zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys (succInjective _ _ p))
288−
289−||| Combine three lists of the same length elementwise using some function.
281+zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) -> List c
282+zipWith f [] (y::ys) = []
283+zipWith f (x::xs) [] = []
284+zipWith f [] [] = []
285+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
286+
287+||| Combine three lists elementwise using some function. If they are different
288+||| lengths, the result is truncated to the length of the shortest list.
290289||| @ f the function to combine elements with
291290||| @ x the first list
292291||| @ y the second list
293292||| @ z the third list
294−||| @ ok a proof that the lengths of the first two inputs are equal
295−||| @ ok' a proof that the lengths of the second and third inputs are equal
296293zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
297− (z : List c) -> (ok : length x = length y) -> (ok' : length y = length z) -> List d
298−zipWith3 f _ [] (z::zs) p Refl impossible
299−zipWith3 f _ (y::ys) [] p Refl impossible
300−zipWith3 f [] (y::ys) _ Refl q impossible
301−zipWith3 f (x::xs) [] _ Refl q impossible
302−zipWith3 f [] [] [] p q = []
303−zipWith3 f (x::xs) (y::ys) (z::zs) p q =
304− f x y z :: (zipWith3 f xs ys zs (succInjective _ _ p) (succInjective _ _ q))
294+ (z : List c) -> List d
295+zipWith3 f _ [] (z::zs) = []
296+zipWith3 f _ (y::ys) [] = []
297+zipWith3 f [] (y::ys) _ = []
298+zipWith3 f (x::xs) [] _ = []
299+zipWith3 f [] [] [] = []
300+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
305301
306302||| Combine two lists elementwise into pairs
307−zip : (l : List a) -> (r : List b) -> (length l = length r) -> List (a, b)
303+zip : (l : List a) -> (r : List b) -> List (a, b)
308304zip = zipWith (\x,y => (x, y))
309305
310306||| Combine three lists elementwise into tuples
311−zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
312− (length y = length z) -> List (a, b, c)
307+zip3 : (x : List a) -> (y : List b) -> (z : List c) -> List (a, b, c)
313308zip3 = zipWith3 (\x,y,z => (x, y, z))
314309
315310||| Split a list of pairs into two lists