summaryrefslogtreecommitdiff
path: root/language/l2.ott
diff options
context:
space:
mode:
Diffstat (limited to 'language/l2.ott')
-rw-r--r--language/l2.ott4
1 files changed, 2 insertions, 2 deletions
diff --git a/language/l2.ott b/language/l2.ott
index f0edda3f..5d1994e2 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -561,7 +561,7 @@ exp :: 'E_' ::=
% here the expi are of type 'a and the result is a vector of 'a, whereas in exp1 : ... : expn
% the expi and the result are both of type vector of 'a
- | [ num1 = exp1 , ... , numn = expn , opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }}
+ | [ num1 = exp1 , ... , numn = expn opt_default ] :: :: vector_indexed {{ com vector (indexed consecutively) }}
% num1 .. numn must be a consecutive list of naturals
% we pick [ ] not { } for vector literals for consistency with their
@@ -661,7 +661,7 @@ opt_default :: 'Def_val_' ::=
{{ com Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map }}
{{ aux _ annot }} {{ auxparam 'a }}
| :: :: empty
- | default = exp :: :: dec
+ | ; default = exp :: :: dec
pexp :: 'Pat_' ::=
{{ com Pattern match }}