Add %elim to Ordering.
commit34d1aca05cf94ae68b3b6b0c20e40b91e95e4896
authorJuliusz Chroboczek <jch@pps.univ-paris-diderot.fr>
dateThu 13 Nov 2014, 19:40 (12 years ago)
parentb83380e
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