blob: 92de65e8011f86afb2c28e01bc5aa9378bf5570d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
module Type
infixr 9 ~>
public export
data Ty : Type where
N : Ty
(~>) : 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')
|
