From 6ce6cf4580f2c0ab4c7c4ec56f438c1cc184c7cd Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 12 Nov 2024 18:05:25 +0000
Subject: Add more names. Names are good.

---
 src/Inky/Decidable.idr | 18 ------------------
 1 file changed, 18 deletions(-)

(limited to 'src/Inky/Decidable.idr')

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
-- 
cgit v1.2.3