Add compilation to scheme.

Extract parser as an independent project.

1 files changed, 3 insertions, 10 deletions

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.(>=>)
 
@@ -85,13 +85,6 @@ data NotFunction : (bound : List String) -> (a : Ty tyCtx) -> Type
 %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')
 isFunctionUnique Done Done = (Refl, Refl)