6638f64 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some things in the prelude

commit6638f640c40b61b00fcc5318973878efe1ac1f51 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 26 Oct 2011, 10:36 (15 years ago) parentb8a2bbf

4 files changed+36

compare with master

unifiedsplit

lib/builtins.idr+17 lib/list.idr+11 lib/maybe.idr+7 lib/prelude.idr+1

lib/builtins.idr+17

@@ -21,14 +21,31 @@ infixl 9 .;

2121(.) : (b -> c) -> (a -> b) -> a -> c;

2222(.) f g x = f (g x);

2323

24+infixr 1 $;

25+

26+($) : (a -> b) -> a -> b;

27+f $ a = f a;

28+

2429data Bool = False | True;

2530

2631boolElim : (x:Bool) -> a -> a -> a;

2732boolElim True t e = t;

2833boolElim False t e = e;

2934

35+data so : Bool -> Set where oh : so True;

36+

3037syntax if [test] then [t] else [e] = boolElim test t e;

3138

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+

3249infixl 5 ==, /=, ==.;

3350infixl 6 <, <=, >, >=, <., <=., >., >=.;

3451infixl 7 <<, >>;

lib/list.idr+11

@@ -13,3 +13,14 @@ rev xs = revAcc Nil xs

1313length : List a -> Int;

1414length Nil = 0;

1515length (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 @@

2+data Maybe a = Nothing | Just a;

4+maybe : b -> (a -> b) -> Maybe a -> b;

5+maybe n j Nothing = n;

6+maybe n j (Just x) = j x;

lib/prelude.idr+1

@@ -1,6 +1,7 @@

11import builtins;

22import nat;

33import list;

4+import maybe;

45import vect;

56import io;