add Uninhabited instances for Maybe
commit95cb7b4115fb40bf3d19b86884596e06fcee99c7
authorAlex Gryzlov <alexander.gryzlov@adform.com>
dateTue 2 Jan 2018, 15:07 (9 years ago)
parent86e5546
libs/prelude/Prelude/Maybe.idr+6
@@ -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