@@ -50,13 +50,13 @@ instance DecEq Bool where
51--------------------------------------------------------------------------------
51--------------------------------------------------------------------------------
53−total OnotS : Z = S n -> Void
53+total ZnotS : Z = S n -> Void
54−OnotS Refl impossible
54+ZnotS Refl impossible
56instance DecEq Nat where
56instance DecEq Nat where
57 decEq Z Z = Yes Refl
57 decEq Z Z = Yes Refl
58− decEq Z (S _) = No OnotS
58+ decEq Z (S _) = No ZnotS
59− decEq (S _) Z = No (negEqSym OnotS)
59+ decEq (S _) Z = No (negEqSym ZnotS)
60 decEq (S n) (S m) with (decEq n m)
60 decEq (S n) (S m) with (decEq n m)
61 | Yes p = Yes $ cong p
61 | Yes p = Yes $ cong p
62 | No p = No $ \h : (S n = S m) => p $ succInjective n m h
62 | No p = No $ \h : (S n = S m) => p $ succInjective n m h