From 29a05f990dd945be30995c4f46b91b5f7c83abd9 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 4 Jul 2023 13:20:46 +0100
Subject: Make unions a pseudo-built-in type.

---
 src/Term/Syntax.idr | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

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

diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index 0ba09a2..d403440 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -43,8 +43,23 @@ t `mod` u = App (App (Op Mod) t) u
 
 export
 Arb : {ty : Ty} -> Term ty ctx
-Arb {ty = N} = Zero
-Arb {ty = ty ~> ty'} = Const Arb
+Arb = Op (Arb ty)
+
+export
+inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
+inL = Op (Inl ty1 ty2)
+
+export
+inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx
+inR = Op (Inr ty1 ty2)
+
+export
+prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx
+prL = Op (Prl ty1 ty2)
+
+export
+prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
+prR = Op (Prr ty1 ty2)
 
 -- HOAS
 
-- 
cgit v1.2.3