Closed pietervdvn closed 9 years ago
The : means that the type on the left is a subclass from the type on the right. E.g. in type declarations (a:Eq), category decls: cat Map k v : Set k.
:
(a:Eq)
cat Map k v : Set k
For multiple subclassing, both "&" and "," should be possible: (a:Eq & Ord), (a:Eq, Ord); cat Map k v : Set k, List b, cat X a b: Monad a & List b
(a:Eq & Ord)
(a:Eq, Ord)
cat Map k v : Set k, List b
cat X a b: Monad a & List b
,
&
The
:
means that the type on the left is a subclass from the type on the right. E.g. in type declarations(a:Eq)
, category decls:cat Map k v : Set k
.For multiple subclassing, both "&" and "," should be possible:
(a:Eq & Ord)
,(a:Eq, Ord)
;cat Map k v : Set k, List b
,cat X a b: Monad a & List b
,
or&
. Also see #54