diff options
| author | Alasdair Armstrong | 2017-11-15 17:31:51 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-15 17:31:51 +0000 |
| commit | 74d2157a022ce0036a1513bd2dada5fb55b71719 (patch) | |
| tree | d8befa5a63387301816db0367e24194b0e20bc9e /language | |
| parent | bb18d5067a46b9e71f57285abce41c1f89e87812 (diff) | |
| parent | ab2b7e532247e03fc6c4e2ca0ccd139e7a4aca0f (diff) | |
Merge branch 'smt' into experiments
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_' ::= |