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.idr | 1 -
 1 file changed, 1 deletion(-)

(limited to 'src/Term.idr')

diff --git a/src/Term.idr b/src/Term.idr
index f6fecbb..b6367a1 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -27,7 +27,6 @@ data Operator : List Ty -> Ty -> Type where
   Inr : (ty, ty' : Ty) -> Operator [ty'] (ty <+> ty')
   Prl : (ty, ty' : Ty) -> Operator [ty <+> ty'] ty
   Prr : (ty, ty' : Ty) -> Operator [ty <+> ty'] ty'
-  Arb : (ty : Ty) -> Operator [] ty
 
 %name Operator op
 
-- 
cgit v1.2.3