git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1713 from jech/add-elim
d8cfafdEdwin Brady
libs/prelude/Builtins.idr+1−1
compare with master
unifiedsplit
@@ -12,7 +12,7 @@
12||| The non-dependent pair type, also known as conjunction.
12||| The non-dependent pair type, also known as conjunction.
13||| @A the type of the left elements in the pair
13||| @A the type of the left elements in the pair
14||| @B the type of the left elements in the pair
14||| @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
16 ||| A pair of elements
16 ||| A pair of elements
17 ||| @a the left element of the pair
17 ||| @a the left element of the pair
18 ||| @b the right element of the pair
18 ||| @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
57
57
58
58
59-- ---------------------------------------------------------- [ Ordering Class ]
59-- ---------------------------------------------------------- [ Ordering Class ]
60−data Ordering = LT | EQ | GT
60+%elim data Ordering = LT | EQ | GT
61
61
62instance Eq Ordering where
62instance Eq Ordering where
63 LT == LT = True
63 LT == LT = True
libs/prelude/Prelude/Either.idr+1−1
@@ -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