git.iko.soy/Idris-dev
on master help sign in
Some things in the prelude
6638f64Edwin Brady
lib/builtins.idr+17
compare with master
unifiedsplit
@@ -21,14 +21,31 @@ infixl 9 .;
21(.) : (b -> c) -> (a -> b) -> a -> c;
21(.) : (b -> c) -> (a -> b) -> a -> c;
22(.) f g x = f (g x);
22(.) f g x = f (g x);
23
23
24+infixr 1 $;
25+
26+($) : (a -> b) -> a -> b;
27+f $ a = f a;
28+
24data Bool = False | True;
29data Bool = False | True;
25
30
26boolElim : (x:Bool) -> a -> a -> a;
31boolElim : (x:Bool) -> a -> a -> a;
27boolElim True t e = t;
32boolElim True t e = t;
28boolElim False t e = e;
33boolElim False t e = e;
29
34
35+data so : Bool -> Set where oh : so True;
36+
30syntax if [test] then [t] else [e] = boolElim test t e;
37syntax if [test] then [t] else [e] = boolElim test t e;
31
38
39+infix 4 &&, ||;
40+
41+(||) : Bool -> Bool -> Bool;
42+(||) False x = x;
43+(||) True _ = True;
44+
45+(&&) : Bool -> Bool -> Bool;
46+(&&) True x = x;
47+(&&) False _ = False;
48+
32infixl 5 ==, /=, ==.;
49infixl 5 ==, /=, ==.;
33infixl 6 <, <=, >, >=, <., <=., >., >=.;
50infixl 6 <, <=, >, >=, <., <=., >., >=.;
34infixl 7 <<, >>;
51infixl 7 <<, >>;
lib/list.idr+11
@@ -13,3 +13,14 @@ rev xs = revAcc Nil xs
13length : List a -> Int;
13length : List a -> Int;
14length Nil = 0;
14length Nil = 0;
15length (Cons x xs) = 1 + length xs;
15length (Cons x xs) = 1 + length xs;
16+
17+take : Int -> List a -> List a;
18+take 0 xs = Nil;
19+take n Nil = Nil;
20+take n (Cons x xs) = Cons x (take (n-1) xs);
21+
22+drop : Int -> List a -> List a;
23+drop 0 xs = xs;
24+drop n Nil = Nil;
25+drop n (Cons x xs) = drop (n-1) xs;
26+
lib/maybe.idrnew file+7
@@ -0,0 +1,7 @@
1+
2+data Maybe a = Nothing | Just a;
3+
4+maybe : b -> (a -> b) -> Maybe a -> b;
5+maybe n j Nothing = n;
6+maybe n j (Just x) = j x;
7+
lib/prelude.idr+1
@@ -1,6 +1,7 @@
1import builtins;
1import builtins;
2import nat;
2import nat;
3import list;
3import list;
4+import maybe;
4import vect;
5import vect;
5import io;
6import io;
6
7