diff options
| author | Peter Sewell | 2013-06-28 08:25:41 +0100 |
|---|---|---|
| committer | Peter Sewell | 2013-06-28 08:25:41 +0100 |
| commit | 65c5f6dc271578ac0ac9da797ad03930abf535b2 (patch) | |
| tree | 01577f4095447fc374797b8dc2968b5c3a6525d6 /language | |
| parent | 1a30923d4d13e235a5a81148adca238f5389cc9c (diff) | |
tweaks from chat with AndrewK, K, P
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/language/l2.ott b/language/l2.ott index 73a1e548..3234a8e4 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -350,8 +350,9 @@ typ :: 'Typ_' ::= % TODO: concrete syntax for effects in a function type? needed only for pp, not in user syntax. | typ1 * .... * typn :: :: tup {{ com Tuple types }} - | nexp :: :: nexps + | nexp :: :: nexps {{ com here to permit applications to nexps, otherwise not accepted }} +% TODO union in the other kind grammars? or make a syntax of argument? or glom together the grammars and leave o the typechecker | id typ1 .. typn :: :: app {{ com Type applications }} | ( typ ) @@ -409,6 +410,9 @@ nexp_constraint :: 'NC_' ::= typquant :: 'TQ_' ::= {{ aux _ l }} | forall id1 ... idn . nexp_constraint1 , ... , nexp_constrainti . :: :: Ts {{ texlong }} + +% WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE + | forall id1 ... idn . :: :: Ts_no_constraint {{ com sugar }} | :: :: Ts_no_forall {{ com sugar }} |