diff options
| author | Peter Sewell | 2017-02-10 13:27:20 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-02-10 13:27:20 +0000 |
| commit | dfc2d8a381c8e11ac175d220dd3226a97cb38514 (patch) | |
| tree | e08ceaf6f18ac0f92086a2cda6b740ac5fb379bb | |
| parent | db7afe68f15814fa3a1b05ffb97fb45fa21b58fa (diff) | |
wib
| -rw-r--r-- | language/l2.ott | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/language/l2.ott b/language/l2.ott index daf9a974..f2603a05 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -324,7 +324,7 @@ typquant :: 'TypQ_' ::= {{ aux _ l }} | forall quant_item1 , ... , quant_itemn . :: :: tq %{{ texlong }} % WHY ARE CONSTRAINTS HERE AND NOT IN THE KIND LANGUAGE - | :: :: no_forall {{ com sugar, omitting quantifier and constraints }} + | :: :: no_forall {{ com empty }} typschm :: 'TypSchm_' ::= {{ com type scheme }} @@ -835,10 +835,10 @@ letbind :: 'LB_' ::= {{ com Let binding }} {{ aux _ annot }} {{ auxparam 'a }} | let typschm pat = exp :: :: val_explicit - {{ com value binding, explicit type ([[pat]] must be total)}} + {{ com let, explicit type ([[pat]] must be total)}} % at the moment, we cannot parse the following, so perhaps we shouldn't keep this form here | let pat = exp :: :: val_implicit - {{ com value binding, implicit type ([[pat]] must be total)}} + {{ com let, implicit type ([[pat]] must be total)}} val_spec :: 'VS_' ::= @@ -882,7 +882,8 @@ reg_id :: 'RI_' ::= | id :: :: id alias_spec :: 'AL_' ::= - {{ com Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector }} + {{ com Register alias expression forms }} +%. Other than where noted, each id must refer to an unaliased register of type vector {{ aux _ annot }} {{ auxparam 'a }} | reg_id . id :: :: subreg | reg_id [ exp ] :: :: bit |