diff options
| author | Peter Sewell | 2017-02-05 11:25:51 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-02-05 11:25:51 +0000 |
| commit | 081d3ac6a786fdc3df515de58af2ef25a25a5b58 (patch) | |
| tree | 1fc083bdfff5a7c5112eb92c66838857d918dec1 | |
| parent | db4d71f55e40747538c4df601fa5f4f6b0e6b0b6 (diff) | |
wib
| -rw-r--r-- | language/l2.ott | 6 | ||||
| -rw-r--r-- | language/manual.pdf | bin | 361603 -> 391550 bytes |
2 files changed, 3 insertions, 3 deletions
diff --git a/language/l2.ott b/language/l2.ott index 84e92d7d..efed02bd 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -162,16 +162,16 @@ kind :: 'K_' ::= % we'll never use ...-> Nat , .. Order , .. or Effects nexp :: 'Nexp_' ::= - {{ com expression of kind Nat, for vector sizes and origins }} + {{ com expression of kind [[Nat]], for vector sizes and origins }} {{ aux _ l }} - | id :: :: id {{ com identifier, bound by def Nat x = nexp }} + | id :: :: id {{ com identifier, bound by \texttt{def Nat x = nexp} }} | 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 :: :: neg {{ com For internal use }} + | neg nexp :: I :: neg {{ com for internal use only}} | ( nexp ) :: S :: paren {{ ichlo [[nexp]] }} order :: 'Ord_' ::= diff --git a/language/manual.pdf b/language/manual.pdf Binary files differindex 22b4c5c3..d848b8da 100644 --- a/language/manual.pdf +++ b/language/manual.pdf |