From 46b29b8e72e171e8a79370d0931aa060442cbbb4 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 9 Apr 2022 18:54:47 +0200
Subject: [PATCH] more ScopeTerm stuff

---
 src/Quox.idr       |  2 +-
 src/Quox/Equal.idr | 10 ++++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Quox.idr b/src/Quox.idr
index 8045498..2840c2c 100644
--- a/src/Quox.idr
+++ b/src/Quox.idr
@@ -26,7 +26,7 @@ banner = #"""
 export
 tm : Term 1 2
 tm =
-  (Pi Zero One "a" (BVT 0) (E (F "F" :@@ [BVT 0, FT "w"]))
+  (Pi Zero One "a" (BVT 0) (TUsed $ E (F "F" :@@ [BVT 0, FT "w"]))
     `DCloT` (K One ::: id))
     `CloT`  (F "y" ::: TYPE (U 1) :# TYPE (U 2) ::: id)
 
diff --git a/src/Quox/Equal.idr b/src/Quox/Equal.idr
index 2853ca6..7888262 100644
--- a/src/Quox/Equal.idr
+++ b/src/Quox/Equal.idr
@@ -46,12 +46,12 @@ parameters {auto _ : MonadThrow Error m}
       eq ClashQ qtm1 qtm2
       eq ClashQ qty1 qty2
       equalT0 arg1 arg2
-      equalT0 res1 res2
+      equalTS0 res1 res2
     equalTN' s@(Pi {}) t _ _ = clashT s t
 
     -- [todo] eta
     equalTN' (Lam _ body1) (Lam _ body2) _ _ =
-      equalT0 body1 body2
+      equalTS0 body1 body2
     equalTN' s@(Lam {}) t _ _ = clashT s t
 
     equalTN' (E e) (E f) ps pt = equalE0 e f
@@ -113,3 +113,9 @@ parameters {auto _ : MonadThrow Error m}
     export covering %inline
     equalE0 : Elim 0 n -> Elim 0 n -> m ()
     equalE0 e f = whnfE e `equalEN` whnfE f
+
+    export covering %inline
+    equalTS0 : ScopeTerm 0 n -> ScopeTerm 0 n -> m ()
+    equalTS0 (TUnused body1) (TUnused body2) = equalT0 body1 body2
+    equalTS0 body1 body2 =
+      fromScopeTerm body1 `equalT0` fromScopeTerm body2