diff options
| author | Peter Sewell | 2013-07-23 15:39:17 +0100 |
|---|---|---|
| committer | Peter Sewell | 2013-07-23 15:39:17 +0100 |
| commit | 33c8450d506db246be6255edcd17b601783c882f (patch) | |
| tree | 9950d164683a3e6efeb8424109497c025c3b3263 /language | |
| parent | ec3f9bb2ee4ef6ead219596e832e5ced32ed8638 (diff) | |
wib
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 2 | ||||
| -rw-r--r-- | language/l2_parse.ott | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/language/l2.ott b/language/l2.ott index 47283a84..4bcd1ba3 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -392,7 +392,7 @@ typ_lib :: 'Typ_lib_' ::= | nat :: :: nat {{ com natural numbers 0,1,2,... }} | string :: :: string {{ com UTF8 strings }} % finite subranges of nat - | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }} + | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by $[[order]]$ }} | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} | [ nexp '..' nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} % use .. not - to avoid ambiguity with nexp - diff --git a/language/l2_parse.ott b/language/l2_parse.ott index 0481c602..4112701d 100644 --- a/language/l2_parse.ott +++ b/language/l2_parse.ott @@ -360,7 +360,7 @@ typ_lib :: 'Typ_lib_' ::= | nat :: :: nat {{ com natural numbers 0,1,2,... }} | string :: :: string {{ com UTF8 strings }} % finite subranges of nat - | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by [[order]] }} + | enum nexp1 nexp2 order :: :: enum {{ com natural numbers [[nexp2]] .. [[nexp2]]+[[nexp1]]-1, ordered by order }} | [ nexp ] :: :: enum1 {{ com sugar for \texttt{enum nexp 0 inc} }} | [ nexp '..' nexp' ] :: :: enum2 {{ com sugar for \texttt{enum (nexp'-nexp+1) nexp inc} or \texttt{enum (nexp-nexp'+1) nexp' dec} }} % use .. not - to avoid ambiguity with nexp - |