git.iko.soy/Idris-dev
on master help sign in
either.idr
da5e25eEdwin Brady
lib/either.idrnew file+8
compare with master
unifiedsplit
@@ -0,0 +1,8 @@
1+import builtins;
2+
3+data Either a b = Left a | Right b;
4+
5+choose : (b : Bool) -> Either (so b) (so (not b));
6+choose True = Left oh;
7+choose False = Right oh;
8+
lib/prelude.idr+1
@@ -2,6 +2,7 @@ import builtins;
2import nat;
2import nat;
3import list;
3import list;
4import maybe;
4import maybe;
5+import either;
5import vect;
6import vect;
6import io;
7import io;
7
8