uninhabited instance for (S n = Z)
commit8ede2ea9d25c9e1e3187f81bed7cc7b9d73e05bb
authorAlex Gryzlov <skyrodent@gmail.com>
dateTue 17 Oct 2017, 01:03 (9 years ago)
parent9e1c9a3
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