on master help sign in
Generalize list eliminator
dda9b49Ben
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
182||| @ nil what to return at the end of the list
182||| @ nil what to return at the end of the list
183||| @ cons what to do at each step of recursion
183||| @ cons what to do at each step of recursion
184||| @ xs the list to recurse over
184||| @ 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
186list nil cons [] = nil
186list nil cons [] = nil
187list nil cons (x::xs) = cons x xs
187list nil cons (x::xs) = cons x xs
188
188