From 33abbf659e337d62b06a16fa01a994fa091080c3 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 24 Jun 2023 14:27:23 +0200
Subject: [PATCH] remove stray comment

---
 lib/Quox/Syntax/Term/Base.idr | 1 -
 1 file changed, 1 deletion(-)

diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 0ff7b3b..994b570 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -133,7 +133,6 @@ data Term where
   ||| dimension closure/suspended substitution
   DCloT : WithSubst (\d => Term d n) Dim d -> Term d n
 
-||| first argument `d` is dimension scope size, second `n` is term scope size
 public export
 data Elim where
   ||| free variable, possibly with a displacement (see @crude, or @mugen for a