Merge pull request #3 from nlogax/master
Add head and tail for lists
commitb63e9bb22c9a4a8e30ad15759b010da2c41d0f97
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateSat 21 Jan 2012, 07:47 (15 years ago)
parent6807cf464a2bc8
lib/prelude/list.idr+8
@@ -19,6 +19,14 @@ app : List a -> List a -> List a
1919app [] xs = xs
2020app (x :: xs) ys = x :: app xs ys
2121
22+head : List a -> Maybe a
23+head [] = Nothing
24+head (x :: xs) = Just x
25+
26+tail : List a -> List a
27+tail [] = []
28+tail (x :: xs) = xs
29+
2230length : List a -> Int
2331length [] = 0
2432length (x :: xs) = 1 + length xs