Merge pull request #1713 from jech/add-elim
Add %elim to various types
commitd8cfafd1e2a3387aa022bedddd26b3ffbe117dc1
authorEdwin Brady <edwin.brady@gmail.com>
dateMon 24 Nov 2014, 11:17 (12 years ago)
parente71676e34d1aca
libs/prelude/Builtins.idr+1−1
@@ -12,7 +12,7 @@
1212||| The non-dependent pair type, also known as conjunction.
1313||| @A the type of the left elements in the pair
1414||| @B the type of the left elements in the pair
15−data Pair : (A : Type) -> (B : Type) -> Type where
15+%elim data Pair : (A : Type) -> (B : Type) -> Type where
1616 ||| A pair of elements
1717 ||| @a the left element of the pair
1818 ||| @b the right element of the pair
libs/prelude/Prelude/Classes.idr+1−1
@@ -57,7 +57,7 @@ instance (Eq a, Eq b) => Eq (a, b) where
5757
5858
5959-- ---------------------------------------------------------- [ Ordering Class ]
60−data Ordering = LT | EQ | GT
60+%elim data Ordering = LT | EQ | GT
6161
6262instance Eq Ordering where
6363 LT == LT = True
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