git.iko.soy/Idris-dev
on master help sign in
Add %elim to Either.
b83380eJuliusz Chroboczek
libs/prelude/Prelude/Either.idr+1−1
compare with master
unifiedsplit
@@ -6,7 +6,7 @@ import Prelude.Maybe
6import Prelude.List
6import Prelude.List
7
7
8||| A sum type
8||| A sum type
9−data Either a b =
9+%elim data Either a b =
10 ||| One possibility of the sum, conventionally used to represent errors
10 ||| One possibility of the sum, conventionally used to represent errors
11 Left a |
11 Left a |
12 ||| The other possibility, conventionally used to represent success
12 ||| The other possibility, conventionally used to represent success