@@ -7,6 +7,7 @@ import Prelude.Bool
77import Prelude.Cast
88import Prelude.Interfaces
99import Prelude.Foldable
10+import Prelude.Uninhabited
1011
1112%access public export
1213%default total
@@ -38,6 +39,14 @@ isJust (Just j) = True
3839data IsJust : Maybe a -> Type where
3940 ItIsJust : IsJust (Just x)
4041
42+Uninhabited (IsJust Nothing) where
43+ uninhabited ItIsJust impossible
44+
45+||| Decide whether a 'Maybe' is 'Just'
46+isItJust : (v : Maybe a) -> Dec (IsJust v)
47+isItJust (Just x) = Yes ItIsJust
48+isItJust Nothing = No absurd
49+
4150--------------------------------------------------------------------------------
4251-- Misc
4352--------------------------------------------------------------------------------