From 3caa95a139538bb07c74847ca3aba2603a03c502 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Fri, 15 Nov 2024 15:44:30 +0000
Subject: Add compilation to scheme.

Extract parser as an independent project.
---
 src/Inky/Term.idr | 13 +++----------
 1 file changed, 3 insertions(+), 10 deletions(-)

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

diff --git a/src/Inky/Term.idr b/src/Inky/Term.idr
index 3c5d214..884256f 100644
--- a/src/Inky/Term.idr
+++ b/src/Inky/Term.idr
@@ -5,9 +5,9 @@ import public Inky.Type
 import Data.List.Quantifiers
 import Data.Singleton
 import Data.These
-import Inky.Data.SnocList.Quantifiers
-import Inky.Decidable
-import Inky.Decidable.Maybe
+import Flap.Data.SnocList.Quantifiers
+import Flap.Decidable
+import Flap.Decidable.Maybe
 
 %hide Prelude.Ops.infixl.(>=>)
 
@@ -84,13 +84,6 @@ data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type
 %name IsFunction prf
 %name NotFunction contra
 
-export
-isFunctionRecompute :
-  {a : Ty tyCtx} -> IsFunction bound a dom cod -> (Singleton dom, Singleton cod)
-isFunctionRecompute Done = (Val _, Val _)
-isFunctionRecompute (Step {a} prf) =
-  mapFst (\case Val _ => Val _) $ isFunctionRecompute prf
-
 export
 isFunctionUnique :
   IsFunction bound a dom cod -> IsFunction bound a dom' cod' -> (dom = dom', cod = cod')
-- 
cgit v1.2.3