diff options
Diffstat (limited to 'src/Inky/Decidable.idr')
| -rw-r--r-- | src/Inky/Decidable.idr | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/src/Inky/Decidable.idr b/src/Inky/Decidable.idr index 860f9e2..7fba676 100644 --- a/src/Inky/Decidable.idr +++ b/src/Inky/Decidable.idr @@ -15,7 +15,6 @@ import Data.These import Data.Vect import Decidable.Equality -import Inky.Data.Irrelevant public export When : Type -> Bool -> Type @@ -39,23 +38,6 @@ toDec : Dec' a -> Dec a toDec (True `Because` prf) = Yes prf toDec (False `Because` contra) = No contra --- So - -public export -decSo : (b : Bool) -> Dec' (So b) -decSo b = b `Because` (if b then Oh else absurd) - --- Irrelevant - -public export -forgetWhen : {b : Bool} -> a `When` b -> Irrelevant a `When` b -forgetWhen {b = True} prf = Forget prf -forgetWhen {b = False} contra = \prf => void $ contra $ prf.value - -public export -(.forget) : Dec' a -> Dec' (Irrelevant a) -p.forget = p.does `Because` forgetWhen p.reason - -- Negation public export |