Generalize list eliminator
Generalize the list eliminator to return any type, rather than only the type of the elements in the list. This matches the behavior of other eliminators, such as maybe and either.
commitdda9b4923196be0c4c0e8fb77355d68b7158d26c
authorBen <bmsherman@users.noreply.github.com>
dateTue 29 Apr 2014, 00:59 (13 years ago)
parent1df6fa9
libs/prelude/Prelude/List.idr+1−1
@@ -182,7 +182,7 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
182182||| @ nil what to return at the end of the list
183183||| @ cons what to do at each step of recursion
184184||| @ xs the list to recurse over
185−list : (nil : a) -> (cons : a -> List a -> a) -> (xs : List a) -> a
185+list : (nil : b) -> (cons : a -> List a -> b) -> (xs : List a) -> b
186186list nil cons [] = nil
187187list nil cons (x::xs) = cons x xs
188188