da5e25e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

either.idr

commitda5e25ede1f9f9ba1af0a9af8257c601c257454d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 17 Nov 2011, 16:05 (15 years ago) parent8d83d07

2 files changed+9

unifiedsplit

lib/either.idrnew file+8

@@ -0,0 +1,8 @@

1+import builtins;

3+data Either a b = Left a | Right b;

5+choose : (b : Bool) -> Either (so b) (so (not b));

6+choose True = Left oh;

7+choose False = Right oh;

lib/prelude.idr+1

@@ -2,6 +2,7 @@ import builtins;

22import nat;

33import list;

44import maybe;

5+import either;

56import vect;

67import io;