git.iko.soy/Idris-dev
on 374fc26 help sign in
Idris-dev/lib/list.idr
36 lines 861 B history raw
1import builtins;
3data List a = Nil | Cons a (List a);
5rev : List a -> List a;
6rev xs = revAcc Nil xs where {
7 revAcc : List a -> List a -> List a;
8 revAcc acc Nil = acc;
9 revAcc acc (Cons x xs) = revAcc (Cons x acc) xs;
12length : List a -> Int;
13length Nil = 0;
14length (Cons x xs) = 1 + length xs;
16take : Int -> List a -> List a;
17take 0 xs = Nil;
18take n Nil = Nil;
19take n (Cons x xs) = Cons x (take (n-1) xs);
21drop : Int -> List a -> List a;
22drop 0 xs = xs;
23drop n Nil = Nil;
24drop n (Cons x xs) = drop (n-1) xs;
26map : (a -> b) -> List a -> List b;
27map f Nil = Nil;
28map f (Cons x xs) = Cons (f x) (map f xs);
30filter : (y -> Bool) -> List y -> List y;
31filter pred Nil = Nil;
32filter pred (Cons x xs) with (pred x, filter pred xs) {
33 filter pred (Cons x xs) | (True, fxs) = Cons x fxs;
34 filter pred (Cons x xs) | (False, fxs) = fxs;