@@ -27,6 +27,12 @@ data Maybe : (a : Type) -> Type where
2727-- Syntactic tests
2828--------------------------------------------------------------------------------
2929
30+Uninhabited (Nothing = Just _) where
31+ uninhabited Refl impossible
32+
33+Uninhabited (Just _ = Nothing) where
34+ uninhabited Refl impossible
35+
3036isNothing : Maybe a -> Bool
3137isNothing Nothing = True
3238isNothing (Just j) = False