summaryrefslogtreecommitdiff
path: root/src/Term.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Term.idr')
-rw-r--r--src/Term.idr1
1 files changed, 0 insertions, 1 deletions
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