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/Type.idr | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/Type.idr')

diff --git a/src/Type.idr b/src/Type.idr
index c4ab809..92de65e 100644
--- a/src/Type.idr
+++ b/src/Type.idr
@@ -1,6 +1,6 @@
 module Type
 
-infixr 4 ~>
+infixr 9 ~>
 
 public export
 data Ty : Type where
@@ -8,3 +8,10 @@ data Ty : Type where
   (~>) : Ty -> Ty -> Ty
 
 %name Ty ty
+
+public export
+(<+>) : Ty -> Ty -> Ty
+N <+> N = N
+N <+> (ty2 ~> ty2') = ty2 ~> (N <+> ty2')
+(ty1 ~> ty1') <+> N = ty1 ~> (ty1' <+> N)
+(ty1 ~> ty1') <+> (ty2 ~> ty2') = (ty1 <+> ty2) ~> (ty1' <+> ty2')
-- 
cgit v1.2.3