@@ -7,6 +7,7 @@ import Prelude.Bool
7import Prelude.Cast
7import Prelude.Cast
8import Prelude.Interfaces
8import Prelude.Interfaces
9import Prelude.Foldable
9import Prelude.Foldable
10+import Prelude.Uninhabited
11%access public export
12%access public export
12%default total
13%default total
@@ -38,6 +39,14 @@ isJust (Just j) = True
38data IsJust : Maybe a -> Type where
39data IsJust : Maybe a -> Type where
39 ItIsJust : IsJust (Just x)
40 ItIsJust : IsJust (Just x)
42+Uninhabited (IsJust Nothing) where
43+ uninhabited ItIsJust impossible
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
41--------------------------------------------------------------------------------
50--------------------------------------------------------------------------------
43--------------------------------------------------------------------------------
52--------------------------------------------------------------------------------