Oops: mistakenly reverted to faulty definition of Eq on nats.
commite4cefe84f819f76f90d61eb274c5eb3d8aa8041a
authorDominic Mulligan <dominic.p.mulligan@googlemail.com>
dateWed 8 Feb 2012, 13:45 (15 years ago)
parent7f7cf8c
lib/prelude/nat.idr+1−1
@@ -49,7 +49,7 @@ power base (S exp) = mult base $ power base exp
4949--------------------------------------------------------------------------------
5050
5151instance Eq Nat where
52− Z == Z = True
52+ O == O = True
5353 (S l) == (S r) = l == r
5454 _ == _ = False
5555