diff options
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') |