git.iko.soy/Idris-dev
on 374fc26 help sign in
Idris-dev/lib/either.idr
8 lines 155 B history raw
1import builtins;
3data Either a b = Left a | Right b;
5choose : (b : Bool) -> Either (so b) (so (not b));
6choose True = Left oh;
7choose False = Right oh;