@@ -161,8 +161,7 @@ init' [] = Nothing
161init' (x::xs) =
161init' (x::xs) =
162 case xs of
162 case xs of
163 [] => Just []
163 [] => Just []
164− y::ys =>
164+ y::ys =>
165− -- XXX: Problem with typechecking a "do" block here
166 case init' $ y::ys of
165 case init' $ y::ys of
167 Nothing => Nothing
166 Nothing => Nothing
168 Just j => Just $ x :: j
167 Just j => Just $ x :: j
@@ -274,42 +273,38 @@ instance Functor List where
274-- Zips and unzips
273-- Zips and unzips
275--------------------------------------------------------------------------------
274--------------------------------------------------------------------------------
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.
278||| @ f the function to combine elements with
278||| @ f the function to combine elements with
279||| @ l the first list
279||| @ l the first list
280||| @ r the second list
280||| @ 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) ->
281+zipWith : (f : a -> b -> c) -> (l : List a) -> (r : List b) -> List c
283− (ok : length l = length r) -> List c
284−zipWith f [] (y::ys) Refl impossible
282+zipWith f [] (y::ys) = []
285−zipWith f (x::xs) [] Refl impossible
283+zipWith f (x::xs) [] = []
286−zipWith f [] [] p = []
284+zipWith f [] [] = []
287−zipWith f (x::xs) (y::ys) p = f x y :: (zipWith f xs ys (succInjective _ _ p))
285+zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys
289−||| Combine three lists of the same length elementwise using some function.
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.
290||| @ f the function to combine elements with
289||| @ f the function to combine elements with
291||| @ x the first list
290||| @ x the first list
292||| @ y the second list
291||| @ y the second list
293||| @ z the third list
292||| @ 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
296zipWith3 : (f : a -> b -> c -> d) -> (x : List a) -> (y : List b) ->
293zipWith3 : (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
294+ (z : List c) -> List d
298−zipWith3 f _ [] (z::zs) p Refl impossible
295+zipWith3 f _ [] (z::zs) = []
299−zipWith3 f _ (y::ys) [] p Refl impossible
296+zipWith3 f _ (y::ys) [] = []
300−zipWith3 f [] (y::ys) _ Refl q impossible
297+zipWith3 f [] (y::ys) _ = []
301−zipWith3 f (x::xs) [] _ Refl q impossible
298+zipWith3 f (x::xs) [] _ = []
302−zipWith3 f [] [] [] p q = []
299+zipWith3 f [] [] [] = []
303−zipWith3 f (x::xs) (y::ys) (z::zs) p q =
300+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs
304− f x y z :: (zipWith3 f xs ys zs (succInjective _ _ p) (succInjective _ _ q))
306||| Combine two lists elementwise into pairs
302||| 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)
308zip = zipWith (\x,y => (x, y))
304zip = zipWith (\x,y => (x, y))
310||| Combine three lists elementwise into tuples
306||| Combine three lists elementwise into tuples
311−zip3 : (x : List a) -> (y : List b) -> (z : List c) -> (length x = length y) ->
307+zip3 : (x : List a) -> (y : List b) -> (z : List c) -> List (a, b, c)
312− (length y = length z) -> List (a, b, c)
313zip3 = zipWith3 (\x,y,z => (x, y, z))
308zip3 = zipWith3 (\x,y,z => (x, y, z))
315||| Split a list of pairs into two lists
310||| Split a list of pairs into two lists