git.iko.soy/Idris-dev
on master help sign in
uninhabited instance for (S n = Z)
8ede2eaAlex Gryzlov
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