diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/language/l2.ott b/language/l2.ott index d27648e9..d010bc67 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -198,14 +198,15 @@ kind :: 'K_' ::= nexp :: 'Nexp_' ::= {{ com numeric expression, of kind $[[Nat]]$ }} {{ aux _ l }} - | id :: :: id {{ com abbreviation identifier }} - | kid :: :: var {{ com variable }} - | num :: :: constant {{ com constant }} - | nexp1 * nexp2 :: :: times {{ com product }} - | nexp1 + nexp2 :: :: sum {{ com sum }} - | nexp1 - nexp2 :: :: minus {{ com subtraction }} - | 2** nexp :: :: exp {{ com exponential }} - | neg nexp :: I :: neg {{ com for internal use only}} + | id :: :: id {{ com abbreviation identifier }} + | kid :: :: var {{ com variable }} + | num :: :: constant {{ com constant }} + | id ( nexp1 , ... , nexpn ) :: :: app {{ com app }} + | nexp1 * nexp2 :: :: times {{ com product }} + | nexp1 + nexp2 :: :: sum {{ com sum }} + | nexp1 - nexp2 :: :: minus {{ com subtraction }} + | 2** nexp :: :: exp {{ com exponential }} + | neg nexp :: I :: neg {{ com for internal use only}} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= |