diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-04 13:20:46 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-07-04 13:20:46 +0100 |
| commit | 29a05f990dd945be30995c4f46b91b5f7c83abd9 (patch) | |
| tree | fc68c964af9d02682520592e4566d25030b47031 /src/Type.idr | |
| parent | 8791efda0cf7392144117cf780bfb6d687d2da5e (diff) | |
Make unions a pseudo-built-in type.
Diffstat (limited to 'src/Type.idr')
| -rw-r--r-- | src/Type.idr | 9 |
1 files changed, 8 insertions, 1 deletions
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') |