From f0f44fe7815435836bc625e837e891188ae8d801 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 22 Jan 2024 12:11:20 +0000
Subject: Fix some bug?

I don't really know. I haven't read this in a long time.
---
 src/Term/Syntax.idr | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/Term/Syntax.idr')

diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index d403440..5a134a2 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -43,7 +43,8 @@ t `mod` u = App (App (Op Mod) t) u
 
 export
 Arb : {ty : Ty} -> Term ty ctx
-Arb = Op (Arb ty)
+Arb {ty = N} = Op (Lit 0)
+Arb {ty = ty ~> ty'} = Const Arb
 
 export
 inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
-- 
cgit v1.2.3