Add %elim to Either.
commitb83380e4036dfa6fe309eff08966da23b9404f6e
authorJuliusz Chroboczek <jch@pps.univ-paris-diderot.fr>
dateThu 13 Nov 2014, 19:40 (12 years ago)
parent3d9115a
libs/prelude/Prelude/Either.idr+1−1
@@ -6,7 +6,7 @@ import Prelude.Maybe
66import Prelude.List
77
88||| A sum type
9−data Either a b =
9+%elim data Either a b =
1010 ||| One possibility of the sum, conventionally used to represent errors
1111 Left a |
1212 ||| The other possibility, conventionally used to represent success