git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4274 from clayrat/uninhabited-maybe
4431c5aAhmad Salim Al-Sibahi
libs/prelude/Prelude/Maybe.idr+6
compare with master
unifiedsplit
@@ -27,6 +27,12 @@ data Maybe : (a : Type) -> Type where
27-- Syntactic tests
27-- Syntactic tests
28--------------------------------------------------------------------------------
28--------------------------------------------------------------------------------
29
29
30+Uninhabited (Nothing = Just _) where
31+ uninhabited Refl impossible
32+
33+Uninhabited (Just _ = Nothing) where
34+ uninhabited Refl impossible
35+
30isNothing : Maybe a -> Bool
36isNothing : Maybe a -> Bool
31isNothing Nothing = True
37isNothing Nothing = True
32isNothing (Just j) = False
38isNothing (Just j) = False