From 0880546a61bc0f7070cc924d9ee89a3fd11ec33b Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 7 Apr 2023 17:54:59 +0100
Subject: Correct definition of Eta conversion.

---
 src/Core/Declarative.idr | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index b6cd55e..d326c4e 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -132,7 +132,10 @@ data TermConv where
     TypeWf env f ->
     TermWf env t (Pi n f g) ->
     TermWf env u (Pi n f g) ->
-    TermConv (env :< f) (App (wkn t $ drop (id _) n) a) (App (wkn u $ drop (id _) n) a) g ->
+    TermConv (env :< f)
+      (App (wkn t $ drop (id _) n) (Var Var.here))
+      (App (wkn u $ drop (id _) n) (Var Var.here))
+      g ->
     ---
     TermConv env t u (Pi n f g)
   AppConv :
-- 
cgit v1.2.3