@@ -2,6 +2,8 @@ module Prelude.Bool
22
33import Builtins
44
5+import Prelude.Uninhabited
6+
57||| Boolean Data Type
68data Bool = False | True
79
@@ -16,6 +18,9 @@ boolElim False t e = e
1618||| Defines a predicate on Bool which guarantees that the value is true.
1719data so : Bool -> Type where oh : so True
1820
21+instance Uninhabited (so False) where
22+ uninhabited oh impossible
23+
1924-- Syntactic sugar for boolean elimination.
2025syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)
2126