git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4128 from clayrat/patch-6
de51bb0Ahmad Salim Al-Sibahi
libs/prelude/Prelude/Nat.idr+3
compare with master
unifiedsplit
@@ -25,6 +25,9 @@ import Prelude.Uninhabited
25
25
26Uninhabited (Z = S n) where
26Uninhabited (Z = S n) where
27 uninhabited Refl impossible
27 uninhabited Refl impossible
28+
29+Uninhabited (S n = Z) where
30+ uninhabited Refl impossible
28
31
29--------------------------------------------------------------------------------
32--------------------------------------------------------------------------------
30-- Syntactic tests
33-- Syntactic tests