From 29a05f990dd945be30995c4f46b91b5f7c83abd9 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 4 Jul 2023 13:20:46 +0100 Subject: Make unions a pseudo-built-in type. --- src/Term.idr | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Term.idr') diff --git a/src/Term.idr b/src/Term.idr index 96a0cb5..f6fecbb 100644 --- a/src/Term.idr +++ b/src/Term.idr @@ -23,6 +23,11 @@ data Operator : List Ty -> Ty -> Type where Minus : Operator [N, N] N Div : Operator [N, N] N Mod : Operator [N, N] N + Inl : (ty, ty' : Ty) -> Operator [ty] (ty <+> ty') + 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