@@ -2,6 +2,8 @@ module Prelude.Bool
3import Builtins
3import Builtins
5+import Prelude.Uninhabited
5||| Boolean Data Type
7||| Boolean Data Type
6data Bool = False | True
8data Bool = False | True
@@ -16,6 +18,9 @@ boolElim False t e = e
16||| Defines a predicate on Bool which guarantees that the value is true.
18||| Defines a predicate on Bool which guarantees that the value is true.
17data so : Bool -> Type where oh : so True
19data so : Bool -> Type where oh : so True
21+instance Uninhabited (so False) where
22+ uninhabited oh impossible
19-- Syntactic sugar for boolean elimination.
24-- Syntactic sugar for boolean elimination.
20syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)
25syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)