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.
commit04801ec7d73a013d99bca2210db9a648cc24bfb6
authorBen <bmsherman@users.noreply.github.com>
dateTue 29 Apr 2014, 00:59 (12 years ago)
parent62705e4
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