Merge pull request #4128 from clayrat/patch-6
uninhabited instance for (S n = Z)
commitde51bb0cdddc8abe2a5fffea4f079b2bf177793d
authorAhmad Salim Al-Sibahi <asal@itu.dk>
dateWed 18 Oct 2017, 14:25 (9 years ago)
parentf261e8b8ede2ea
libs/prelude/Prelude/Nat.idr+3
@@ -25,6 +25,9 @@ import Prelude.Uninhabited
2525
2626Uninhabited (Z = S n) where
2727 uninhabited Refl impossible
28+
29+Uninhabited (S n = Z) where
30+ uninhabited Refl impossible
2831
2932--------------------------------------------------------------------------------
3033-- Syntactic tests