From 6da33625f8e7858bf383751ee62b76c9449f71bd Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Fri, 3 Sep 2021 17:54:52 +0200
Subject: [PATCH] remove an (.int). no one likes ints

---
 src/Quox/Syntax/Term.idr | 4 ++++
 src/Quox/Syntax/Var.idr  | 8 --------
 2 files changed, 4 insertions(+), 8 deletions(-)

diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index ff7f2a6..3c0c576 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -277,10 +277,14 @@ NotCloTerm d n = Subset (Term d n) $ So . not . isCloT
 
 
 mutual
+  ||| if the input term has any top-level closures, push them under one layer of
+  ||| syntax
   export
   pushSubstsT : Term d n -> NotCloTerm d n
   pushSubstsT s = pushSubstsT' id id s
 
+  ||| if the input elimination has any top-level closures, push them under one
+  ||| layer of syntax
   export
   pushSubstsE : Elim d n -> NotCloElim d n
   pushSubstsE e = pushSubstsE' id id e
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 976b3d7..ca5747b 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -99,14 +99,6 @@ toFromNat 0     (LTESucc x) = Refl
 toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 
-public export
-(.int) : Var n -> Integer
-i.int = natToInteger i.nat
-%builtin NaturalToInteger Var.(.int)
-
-public export Cast (Var n) Integer where cast i = i.int
-
-
 -- not using %transform like other things because weakSpec requires the proof
 -- to be relevant. but since only `LTESucc` is ever possible that seems
 -- to be a bug?