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/Encoded/Union.idr | 42 ------------------------------------------
 1 file changed, 42 deletions(-)
 delete mode 100644 src/Encoded/Union.idr

(limited to 'src/Encoded/Union.idr')

diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
deleted file mode 100644
index 00b07e7..0000000
--- a/src/Encoded/Union.idr
+++ /dev/null
@@ -1,42 +0,0 @@
-module Encoded.Union
-
-import Term.Syntax
-
--- Binary Union ----------------------------------------------------------------
-
-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')
-
-export
-swap : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> (ty2 <+> ty1)) ctx
-swap {ty1 = N, ty2 = N} = Id
-swap {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f)
-swap {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => swap . f)
-swap {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f . swap)
-
-export
-inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
-export
-prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx
-
-inL {ty1 = N, ty2 = N} = Id
-inL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\n => Const (App inL [<n]))
-inL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => inL . f)
-inL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => inL . f . prL)
-
-prL {ty1 = N, ty2 = N} = Id
-prL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\t => App prL [<App t [<Arb]])
-prL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\t => prL . t)
-prL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\t => prL . t . inL)
-
-export
-inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx
-inR = swap . inL
-
-export
-prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
-prR = prL . swap
-- 
cgit v1.2.3