diff options
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/language/l2.ott b/language/l2.ott index 3bdfeba8..47283a84 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -5,7 +5,7 @@ indexvar n , i , j , k ::= metavar num ::= {{ phantom }} {{ lex numeric }} - {{ ocaml terminal * int }} + {{ ocaml (terminal * int) }} {{ hol num }} {{ lem (terminal * num) }} {{ com Numeric literals }} @@ -332,7 +332,7 @@ order :: 'Ord_' ::= | dec :: :: dec {{ com decreasing (big-endian) }} | ( order ) :: S :: paren {{ icho [[order]] }} -effect :: 'Effect_' ::= +efct :: 'Effect_' ::= {{ com effect }} {{ aux _ l }} | rreg :: :: rreg {{ com read register }} @@ -347,8 +347,8 @@ effect :: 'Effect_' ::= effects :: 'Effects_' ::= {{ com effect set, of kind $[[Effects]]$ }} {{ aux _ l }} - | id :: :: var - | { effect1 , .. , effectn } :: :: set {{ com effect set }} + | effect id :: :: var + | effect { efct1 , .. , efctn } :: :: set {{ com effect set }} | pure :: M :: pure {{ com sugar for empty effect set }} {{ icho [] }} % TODO: are we going to need any effect polymorphism? Conceivably for built-in maps and folds. Yes. But we think we don't need any interesting effect-set expressions, eg effectset-variable union {rreg}. |