diff options
| author | Peter Sewell | 2017-02-13 17:30:44 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-02-13 17:30:44 +0000 |
| commit | 352d86f08d2f18651eeeccdbedb0ff359e312e37 (patch) | |
| tree | 10078af4daa2675058e338228817e7f9758345f2 /language | |
| parent | 0f5eb59075c832fc69d32a9cdf5c417032f2bf9c (diff) | |
make syntax typeset in manual in ASCII-friendly style rather than using
math symbols. This breaks the l2.pdf build in language/ (for the moment).
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2.ott | 41 |
1 files changed, 25 insertions, 16 deletions
diff --git a/language/l2.ott b/language/l2.ott index fe66c8e7..66a4e76d 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -949,23 +949,26 @@ terminals :: '' ::= {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }} {{ com \texttt{**} }} | >= :: :: geq - {{ tex \ensuremath{\geq} }} +% {{ tex \ensuremath{\geq} }} + {{ tex \ottsym{\textgreater=} }} {{ com \texttt{>=} }} | '<=' :: :: leq - {{ tex \ensuremath{\leq} }} +% {{ tex \ensuremath{\leq} }} + {{ tex \ottsym{\textless=} }} {{ com \texttt{<=} }} | -> :: :: arrow - {{ tex \ensuremath{\rightarrow} }} +% {{ tex \ensuremath{\rightarrow} }} + {{ tex \ottsym{-\textgreater} }} {{ com \texttt{->} }} | ==> :: :: Longrightarrow {{ tex \ensuremath{\Longrightarrow} }} {{ com \texttt{==>} }} - | <| :: :: startrec - {{ tex \ensuremath{\langle|} }} - {{ com \texttt{<|} }} - | |> :: :: endrec - {{ tex \ensuremath{|\rangle} }} - {{ com \texttt{|>} }} +% | <| :: :: startrec +% {{ tex \ensuremath{\langle|} }} +% {{ com \texttt{<|} }} +% | |> :: :: endrec +% {{ tex \ensuremath{|\rangle} }} +% {{ com \texttt{|>} }} | inter :: :: inter {{ tex \ensuremath{\cap} }} | u+ :: :: uplus @@ -981,9 +984,11 @@ terminals :: '' ::= | emptyset :: :: emptyset {{ tex \ensuremath{\emptyset} }} | < :: :: lt - {{ tex \ensuremath{\langle} }} +% {{ tex \ensuremath{\langle} }} + {{ tex \ottsym{<} }} | > :: :: gt - {{ tex \ensuremath{\rangle} }} +% {{ tex \ensuremath{\rangle} }} + {{ tex \ottsym{>} }} | lt :: :: mathlt {{ tex < }} | gt :: :: mathgt @@ -1005,7 +1010,7 @@ terminals :: '' ::= | |-c :: :: vdashC {{ tex \ensuremath{\vdash_c} }} | ' :: :: quote - {{ tex \mbox{'} }} + {{ tex \ottsym{'} }} | |-> :: :: mapsto {{ tex \ensuremath{\mapsto} }} | gives :: :: gives @@ -1028,9 +1033,13 @@ terminals :: '' ::= {{ tex \ottkw{consistent\_decrease}~ }} | == :: :: equiv {{ tex \equiv }} -% | [|| :: :: list_start -% {{ tex \ottsym{[||} }} -% | ||] :: :: list_end -% {{ tex \ottsym{||]} }} + | [| :: :: range_start + {{ tex \ottsym{[\textbar} }} + | |] :: :: range_end + {{ tex \ottsym{\textbar]} }} + | [|| :: :: list_start + {{ tex \ottsym{[\textbar\textbar} }} + | ||] :: :: list_end + {{ tex \ottsym{\textbar\textbar]} }} |