diff options
Diffstat (limited to 'language/l2_parse.ott')
| -rw-r--r-- | language/l2_parse.ott | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/language/l2_parse.ott b/language/l2_parse.ott index da3d57ca..3ef811bb 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -106,11 +106,6 @@ l :: '' ::= {{ phantom }} {{ lem Unknown }} {{ hol () }} -annot :: '' ::= - {{ phantom }} - {{ ocaml 'a annot }} - {{ lem annot }} - {{ hol unit }} id :: '' ::= {{ com Identifier }} @@ -173,6 +168,7 @@ atyp :: 'ATyp_' ::= | atyp1 * atyp2 :: :: times {{ com product }} | atyp1 + atyp2 :: :: sum {{ com sum }} | 2** atyp :: :: exp {{ com exponential }} + | neg atyp :: :: neg {{ com Internal (but not M as I want a datatype constructor) negative nexp }} | ( atyp ) :: S :: paren {{ icho [[atyp]] }} | inc :: :: inc {{ com increasing (little-endian) }} |