From 2b756ae1bbb4440679bec03781c6445453059fb6 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 25 May 2022 16:03:23 +0200
Subject: [PATCH] tiny tweak

---
 lib/Quox/Syntax/Term/Base.idr | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Base.idr b/lib/Quox/Syntax/Term/Base.idr
index 6017846..a707495 100644
--- a/lib/Quox/Syntax/Term/Base.idr
+++ b/lib/Quox/Syntax/Term/Base.idr
@@ -90,8 +90,8 @@ mutual
 %name DScopeTerm body
 
 public export %inline
-Arr : Qty -> Term d n -> Term d n -> Term d n
-Arr pi a b = Pi {qty = pi, x = "_", arg = a, res = TUnused b}
+Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
+Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
 
 ||| same as `F` but as a term
 public export %inline