0 | module Data.Bool.Decidable
 1 |
 2 | import Data.Void
 3 |
 4 | public export
 5 | data Reflects : Type -> Bool -> Type where
 6 |   RTrue  :     p -> Reflects p True
 7 |   RFalse : Not p -> Reflects p False
 8 |
 9 | public export
10 | recompute : Dec a -> (0 x : a) -> a
11 | recompute (Yes x) _ = x
12 | recompute (No contra) x = absurdity $ contra x
13 |
14 | public export
15 | invert : {0 b : Bool} -> {0 p : Type} -> Reflects p b -> if b then p else Not p
16 | invert {b = True} (RTrue  x ) = x
17 | invert {b = False} (RFalse nx) = nx
18 |
19 | public export
20 | remember : {b : Bool} -> {0 p : Type} -> (if b then p else Not p) -> Reflects p b
21 | remember {b = True } = RTrue
22 | remember {b = False} = RFalse
23 |
24 | public export
25 | reflect : {c : Bool} -> Reflects p b -> (if c then p else Not p) -> b = c
26 | reflect {c = True } (RTrue   x)  _ = Refl
27 | reflect {c = True } (RFalse nx)  x = absurd $ nx x
28 | reflect {c = False} (RTrue   x) nx = absurd $ nx x
29 | reflect {c = False} (RFalse nx)  _ = Refl
30 |