Changeset 1048b31 for doc

Timestamp:

May 2, 2016, 3:28:16 PM (10 years ago)

Author:

Rob Schluntz <rschlunt@…>

Branches:

ADT, aaron-thesis, arm-eh, ast-experimental, cleanup-dtors, ctor, deferred_resn, demangler, enum, forall-pointer-decay, gc_noraii, jacob/cs343-translation, jenkins-sandbox, master, memory, new-ast, new-ast-unique-expr, new-env, no_list, persistent-indexer, pthread-emulation, qualifiedEnum, resolv-new, with_gc

Children:

1b7ea43

Parents:

1f6e009 (diff), e945826 (diff)
Note: this is a merge changeset, the changes displayed below correspond to the merge itself.
Use the (diff) links above to see all the changes relative to each parent.

Message:

Merge branch 'master' into global-init

Location:

doc

Files:

• LaTeXmacros/common.tex (added)
• LaTeXmacros/indexstyle (moved) (moved from doc/refrat/indexstyle )
• bibliography/cfa.bib (added)
• refrat/Makefile (modified) (3 diffs)
• refrat/refrat.tex (modified) (165 diffs)
• user/Cdecl.fig (added)
• user/Makefile (modified) (4 diffs)
• user/indexstyle (deleted)
• user/user.bib (deleted)
• user/user.tex (modified) (63 diffs)

doc/refrat/Makefile

@@ -1 +1 @@
 ## Define the appropriate configuration variables.
 
-Macros = 
-TeXLIB = .:${Macros}:
+TeXLIB = .:../bibliography/:../LaTeXmacros/:
 LaTeX  = TEXINPUTS=${TeXLIB} && export TEXINPUTS && latex
-BibTeX = BSTINPUTS=${TeXLIB} && export BSTINPUTS && bibtex
+BibTeX = BIBINPUTS=${TeXLIB} && export BIBINPUTS && bibtex
 
 ## Define the text source files.
@@ -44 +43 @@
         dvips $< -o $@
 
-${basename ${DOCUMENT}}.dvi : Makefile ${GRAPHS} ${PROGRAMS} ${PICTURES} ${FIGURES} ${SOURCES} ${basename ${DOCUMENT}}.tex ${basename ${DOCUMENT}}.bib
+${basename ${DOCUMENT}}.dvi : Makefile ${GRAPHS} ${PROGRAMS} ${PICTURES} ${FIGURES} ${SOURCES} ${basename ${DOCUMENT}}.tex \
+                ../LaTeXmacros/common.tex ../LaTeXmacros/indexstyle ../bibliography/cfa.bib
         # Conditionally create an empty *.ind (index) file for inclusion until makeindex is run.
         if [ ! -r ${basename $@}.ind ] ; then touch ${basename $@}.ind ; fi
@@ -54 +54 @@
         -${BibTeX} ${basename $@}
         # Make index from *.aux entries and input index at end of document
-        makeindex -s indexstyle ${basename $@}.idx
+        makeindex -s ../LaTeXmacros/indexstyle ${basename $@}.idx
         ${LaTeX} ${basename $@}.tex
         # Run again to get index title into table of contents

doc/refrat/refrat.tex

@@ +1 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- Mode: Latex -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% 
+%% Cforall Version 1.0.0 Copyright (C) 2016 University of Waterloo
+%%
+%% The contents of this file are covered under the licence agreement in the
+%% file "LICENCE" distributed with Cforall.
+%% 
+%% refrat.tex -- 
+%% 
+%% Author           : Peter A. Buhr
+%% Created On       : Wed Apr  6 14:52:25 2016
+%% Last Modified By : Peter A. Buhr
+%% Last Modified On : Sat Apr 30 13:45:40 2016
+%% Update Count     : 29
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 % requires tex packages: texlive-base texlive-latex-base tex-common texlive-humanities texlive-latex-extra texlive-fonts-recommended
+
+% red highlighting ®...® (registered trademark sumbol)
+% blue highlighting ©...© (copyright symbol)
+% latex escape §...§ (section symbol)
+% keyword escape ¶...¶ (pilcrow symbol)
+% math escape $...$ (dollar symbol)
 
 \documentclass[openright,twoside]{report}
@@ -5 +27 @@
 
 % Latex packages used in the document.
-
 \usepackage{fullpage,times}
 \usepackage{xspace}
@@ -11 +32 @@
 \usepackage{listings}
 \usepackage{comment}
-\usepackage{latexsym}                                   % \Box
-\usepackage{mathptmx}                                   % better math font with "times"
+\usepackage{latexsym}                                   % \Box
+\usepackage{mathptmx}                                   % better math font with "times"
 \usepackage[pagewise]{lineno}
 \renewcommand{\linenumberfont}{\scriptsize\sffamily}
@@ -21 +42 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-% Names used in the document.
-
-\newcommand{\CFA}{C$\forall$\xspace}    % set language symbolic name
-\newcommand{\CFL}{Cforall\xspace}               % set language text name
-\newcommand{\CC}{C\kern-.1em\hbox{+\kern-.25em+}\xspace} % CC symbolic name
-\def\c11{ISO/IEC C} % C11 name (cannot have numbers in latex command name)
+% Bespoke macros used in the document.
+\input{common}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-% Bespoke macros used in the document.
-
-\makeatletter
-% allow escape sequence in lstinline
-%\usepackage{etoolbox}
-%\patchcmd{\lsthk@TextStyle}{\let\lst@DefEsc\@empty}{}{}{\errmessage{failed to patch}}
-
-\renewcommand\small{%
-   \@setfontsize\small{8.5}{11}%
-   \abovedisplayskip 8.5pt \@plus 3pt \@minus 4pt
-   \abovedisplayshortskip \z@ \@plus 2pt
-   \belowdisplayshortskip 4pt \@plus 2pt \@minus 2pt
-   \def\@listi{\leftmargin\leftmargini
-               \topsep 4pt \@plus 2pt \@minus 2pt
-               \parsep 2pt \@pluspt \@minuspt
-               \itemsep \parsep}%
-   \belowdisplayskip \abovedisplayskip
-}
-\usepackage{relsize}            % must be after change to small
-
-\renewcommand{\labelitemi}{{\raisebox{0.25ex}{\footnotesize$\bullet$}}}
-\renewenvironment{itemize}{\begin{list}{\labelitemi}{\topsep=5pt\itemsep=5pt\parsep=0pt}}{\end{list}}
-
-%  Reduce size of chapter/section titles
-\def\@makechapterhead#1{%
-  \vspace*{50\p@}%
-  {\parindent \z@ \raggedright \normalfont
-    \ifnum \c@secnumdepth >\m@ne
-        \large\bfseries \@chapapp\space \thechapter
-        \par\nobreak
-        \vskip 5\p@
-    \fi
-    \interlinepenalty\@M
-    \Large \bfseries #1\par\nobreak
-    \vskip 50\p@
-  }}
-\def\@makeschapterhead#1{%
-  \vspace*{50\p@}%
-  {\parindent \z@ \raggedright
-    \normalfont
-    \interlinepenalty\@M
-    \Large \bfseries  #1\par\nobreak
-    \vskip 50\p@
-  }}
-\renewcommand\section{\@startsection{section}{1}{\z@}{-3.0ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\large\bfseries}}
-\renewcommand\subsection{\@startsection{subsection}{2}{\z@}{-2.5ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\normalsize\bfseries}}
-\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}{-2.5ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\normalsize\bfseries}}
-\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}{-2.0ex \@plus -1ex \@minus -.2ex}{-1em}{\normalfont\normalsize\bfseries}}
-
-% index macros
-\newcommand{\italic}[1]{\emph{\hyperpage{#1}}}
-\newcommand{\definition}[1]{\textbf{\hyperpage{#1}}}
-\newcommand{\see}[1]{\emph{see} #1}
-
-% Define some commands that produce formatted index entries suitable for cross-references.
-% ``\spec'' produces entries for specifications of entities.  ``\impl'' produces entries for their
-% implementations, and ``\use'' for their uses.
-
-%  \newcommand{\bold}[1]{{\bf #1}}
-%  \def\spec{\@bsphack\begingroup
-%             \def\protect##1{\string##1\space}\@sanitize
-%             \@wrxref{|bold}}
-\def\impl{\@bsphack\begingroup
-          \def\protect##1{\string##1\space}\@sanitize
-          \@wrxref{|definition}}
-\newcommand{\indexcode}[1]{{\lstinline$#1$}}
-\def\use{\@bsphack\begingroup
-         \def\protect##1{\string##1\space}\@sanitize
-         \@wrxref{|hyperpage}}
-\def\@wrxref#1#2{\let\thepage\relax
-    \xdef\@gtempa{\write\@indexfile{\string
-    \indexentry{#2@{\lstinline$#2$}#1}{\thepage}}}\endgroup\@gtempa
-    \if@nobreak \ifvmode\nobreak\fi\fi\@esphack}
-%\newcommand{\use}[1]{\index{#1@{\lstinline$#1$}}}
-%\newcommand{\impl}[1]{\index{\protect#1@{\lstinline$\protect#1$}|definition}}
-
-% inline text and lowercase index: \Index{inline and lowercase index text}
-% inline text and as-in index: \Index[as-is index text]{inline text}
-% inline text but index with different as-is text: \Index[index text]{inline text}
-\newcommand{\Index}{\@ifstar\@sIndex\@Index}
-\newcommand{\@Index}[2][\@empty]{\lowercase{\def\temp{#2}}#2\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi}
-\newcommand{\@sIndex}[2][\@empty]{#2\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi}
-\makeatother
-
-% blocks and titles
-\newenvironment{rationale}{%
-  \begin{quotation}\noindent$\Box$\enspace
-}{%
-  \hfill\enspace$\Box$\end{quotation}
-}%
-\newcommand{\define}[1]{\emph{#1\/}\index{#1}}
-\newcommand{\rewrite}{\(\Rightarrow\)}
-\newcommand{\rewriterules}{\paragraph{Rewrite Rules}~\par\noindent}
-\newcommand{\examples}{\paragraph{Examples}~\par\noindent}
-\newcommand{\semantics}{\paragraph{Semantics}~\par\noindent}
-\newcommand{\constraints}{\paragraph{Constraints}~\par\noindent}
-\newcommand{\predefined}{\paragraph{Predefined Identifiers}~\par\noindent}
-
-% BNF macros
-\def\syntax{\paragraph{Syntax}\trivlist\parindent=.5in\item[\hskip.5in]}
-\let\endsyntax=\endtrivlist
-\newcommand{\lhs}[1]{\par{\emph{#1:}}\index{#1@{\emph{#1}}|italic}}
-\newcommand{\rhs}{\hfil\break\hbox{\hskip1in}}
-\newcommand{\oldlhs}[1]{\emph{#1: \ldots}\index{#1@{\emph{#1}}|italic}}
-\newcommand{\nonterm}[1]{\emph{#1\/}\index{#1@{\emph{#1}}|italic}}
-\newcommand{\opt}{$_{opt}$\ }
-
-% adjust varioref package with default "section" and "page" titles, and optional title with faraway page numbers
-% \VRef{label} => Section 2.7, \VPageref{label} => page 17
-% \VRef[Figure]{label} => Figure 3.4, \VPageref{label} => page 17
-\renewcommand{\reftextfaceafter}{\unskip}
-\renewcommand{\reftextfacebefore}{\unskip}
-\renewcommand{\reftextafter}{\unskip}
-\renewcommand{\reftextbefore}{\unskip}
-\renewcommand{\reftextfaraway}[1]{\unskip, p.~\pageref{#1}}
-\renewcommand{\reftextpagerange}[2]{\unskip, pp.~\pageref{#1}--\pageref{#2}}
-\newcommand{\VRef}[2][Section]{\ifx#1\@empty\else{#1}\nobreakspace\fi\vref{#2}}
-\newcommand{\VPageref}[2][page]{\ifx#1\@empty\else{#1}\nobreakspace\fi\pageref{#2}}
-
-% CFA based on ANSI C
-\lstdefinelanguage{CFA}[ANSI]{C}%
-{morekeywords={asm,_Alignas,_Alignof,_At,_Atomic,_Bool,catch,catchResume,choose,_Complex,trait,disable,dtype,enable,
-        fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,lvalue,_Noreturn,otype,restrict,_Static_assert,
-        _Thread_local,throw,throwResume,try,},
-}%
-
-\lstset{
-language=CFA,
-columns=flexible,
-basicstyle=\sf\relsize{-1},
-tabsize=4,
-xleftmargin=\parindent,
-escapechar=@,
-keepspaces=true,
-showstringspaces=false,
-showlines=true,
-}%
-
-\makeatletter
-% replace/adjust listings characters that look bad in sanserif
-\lst@CCPutMacro
-\lst@ProcessOther{"2D}{\lst@ttfamily{-{}}{{\ttfamily\upshape -}}} % replace minus
-\lst@ProcessOther{"3C}{\lst@ttfamily{<}{\texttt{<}}} % replace less than
-\lst@ProcessOther{"3E}{\lst@ttfamily{<}{\texttt{>}}} % replace greater than
-\lst@ProcessOther{"5E}{\raisebox{0.4ex}{$\scriptstyle\land\,$}} % replace circumflex
-\lst@ProcessLetter{"5F}{\lst@ttfamily{\char95}{{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}}} % replace underscore
-\lst@ProcessOther{"7E}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}} % replace tilde
-%\lst@ProcessOther{"7E}{\raisebox{-.4ex}[1ex][0pt]{\textasciitilde}} % lower tilde
-\@empty\z@\@empty
-\makeatother
-
-\setcounter{secnumdepth}{3}     % number subsubsections
-\setcounter{tocdepth}{3}                % subsubsections in table of contents
+\setcounter{secnumdepth}{3}                             % number subsubsections
+\setcounter{tocdepth}{3}                                % subsubsections in table of contents
 \makeindex
 
@@ -189 +55 @@
 \begin{document}
 \pagestyle{headings}
-\linenumbers                                    % comment out to turn off line numbering
+\linenumbers                                            % comment out to turn off line numbering
 
 \title{\Huge
+\vspace*{1in}
 \CFA (\CFL) Reference Manual and Rationale
 }% title
@@ -226 +93 @@
 
 This document is a reference manual and rationale for \CFA, a polymorphic extension of the C programming language.
-It makes frequent reference to the {\c11} standard \cite{ANS:C11}, and occasionally compares \CFA to {\CC} \cite{c++}.
+It makes frequent reference to the {\c11} standard \cite{C11}, and occasionally compares \CFA to {\CC} \cite{C++}.
 
 The manual deliberately imitates the ordering of the {\c11} standard (although the section numbering differs).
@@ -264 +131 @@
 \CFA's scope rules differ from C's in one major respect: a declaration of an identifier may overload\index{overloading} outer declarations of lexically identical identifiers in the same
 \Index{name space}, instead of hiding them.
-The outer declaration is hidden if the two declarations have \Index{compatible type}, or if one declares an array type and the other declares a pointer type and the element type and pointed-at type are compatible, or if one has function type and the other is a pointer to a compatible function type, or if one declaration is a \lstinline$type$\use{type} or
-\lstinline$typedef$\use{typedef} declaration and the other is not.  The outer declaration becomes
+The outer declaration is hidden if the two declarations have \Index{compatible type}, or if one declares an array type and the other declares a pointer type and the element type and pointed-at type are compatible, or if one has function type and the other is a pointer to a compatible function type, or if one declaration is a \lstinline@type@\use{type} or
+\lstinline@typedef@\use{typedef} declaration and the other is not.  The outer declaration becomes
 \Index{visible} when the scope of the inner declaration terminates.
 \begin{rationale}
-Hence, a \CFA program can declare an \lstinline$int v$ and a \lstinline$float v$ in the same scope;
+Hence, a \CFA program can declare an \lstinline@int v@ and a \lstinline@float v@ in the same scope;
 a {\CC} program can not.
 \end{rationale}
@@ -282 +149 @@
 Identifiers with \Index{no linkage} always denote unique entities.
 \begin{rationale}
-A \CFA program can declare an \lstinline$extern int v$ and an \lstinline$extern float v$;
+A \CFA program can declare an \lstinline@extern int v@ and an \lstinline@extern float v@;
 a C program cannot.
 \end{rationale}
@@ -305 +172 @@
 \end{lstlisting}
 
-The type parameters in an instantiation of a generic type must satisfy any constraints in the forall specifier on the type generator declaration, e.g., \lstinline$sumable$.
+The type parameters in an instantiation of a generic type must satisfy any constraints in the forall specifier on the type generator declaration, e.g., \lstinline@sumable@.
 The instantiation then has the semantics that would result if the type parameters were substituted into the type generator declaration by macro substitution.
 
@@ -366 +233 @@
 In \CFA, these conversions play a role in overload resolution, and collectively are called the \define{safe arithmetic conversion}s.
 
-Let \(int_r\) and \(unsigned_r\) be the signed and unsigned integer types with integer conversion rank\index{integer conversion rank}\index{rank|see{integer conversion rank}} $r$.
-Let \(unsigned_{mr}\) be the unsigned integer type with maximal rank.
+Let \lstinline@int$_r$@ and \lstinline@unsigned$_r$@ be the signed and unsigned integer types with integer conversion rank\index{integer conversion rank}\index{rank|see{integer conversion rank}} $r$.
+Let \lstinline@unsigned$_{mr}$@ be the unsigned integer type with maximal rank.
 
 The following conversions are \emph{direct} safe arithmetic conversions.
@@ -374 +241 @@
 The \Index{integer promotion}s.
 \item
-For every rank $r$ greater than or equal to the rank of \lstinline$int$, conversion from \(int_r\) to \(unsigned_r\).
-\item
-For every rank $r$ greater than or equal to the rank of \lstinline$int$, where \(int_{r+1}\) exists and can represent all values of \(unsigned_r\), conversion from \(unsigned_r\) to \(int_{r+1}\).
-\item
-Conversion from \(unsigned_{mr}\) to \lstinline$float$.
+For every rank $r$ greater than or equal to the rank of \lstinline@int@, conversion from \lstinline@int$_r$@ to \lstinline@unsigned$_r$@.
+\item
+For every rank $r$ greater than or equal to the rank of \lstinline@int@, where \lstinline@int$_{r+1}$@ exists and can represent all values of \lstinline@unsigned$_r$@, conversion from \lstinline@unsigned$_r$@ to \lstinline@int$_{r+1}$@.
+\item
+Conversion from \lstinline@unsigned$_{mr}$@ to \lstinline@float@.
 \item
 Conversion from an enumerated type to its compatible integer type.
 \item
-Conversion from \lstinline$float$ to \lstinline$double$, and from \lstinline$double$ to \lstinline$long double$.
-\item
-Conversion from \lstinline$float _Complex$ to \lstinline$double _Complex$, and from \lstinline$double _Complex$ to \lstinline$long double _Complex$.
+Conversion from \lstinline@float@ to \lstinline@double@, and from \lstinline@double@ to \lstinline@long double@.
+\item
+Conversion from \lstinline@float _Complex@ to \lstinline@double _Complex@, and from \lstinline@double _Complex@ to \lstinline@long double _Complex@.
 \begin{sloppypar}
 \item
-Conversion from \lstinline$float _Imaginary$ to \lstinline$double _Imaginary$, and from \lstinline$double _Imaginary$ to \lstinline$long double$ \lstinline$_Imaginary$, if the implementation supports imaginary types.
+Conversion from \lstinline@float _Imaginary@ to \lstinline@double _Imaginary@, and from \lstinline@double _Imaginary@ to \lstinline@long double _Imaginary@, if the implementation supports imaginary types.
 \end{sloppypar}
 \end{itemize}
 
-If type \lstinline$T$ can be converted to type \lstinline$U$ by a safe direct arithmetic conversion and type \lstinline$U$ can be converted to type \lstinline$V$ by a safe arithmetic conversion, then the conversion from \lstinline$T$ to type \lstinline$V$ is an \emph{indirect} safe arithmetic conversion.
+If type \lstinline@T@ can be converted to type \lstinline@U@ by a safe direct arithmetic conversion and type \lstinline@U@ can be converted to type \lstinline@V@ by a safe arithmetic conversion, then the conversion from \lstinline@T@ to type \lstinline@V@ is an \emph{indirect} safe arithmetic conversion.
 
 \begin{rationale}
@@ -414 +281 @@
         int x, y;
 };
-void move_by( struct point * p1, struct point * p2 ) {@\impl{move_by}@
+void move_by( struct point * p1, struct point * p2 ) {§\impl{move_by}§
         p1->x += p2.x;
         p1->y += p2.y;
@@ -424 +291 @@
 move_to( &cp1, &cp2 );
 \end{lstlisting}
-Thanks to implicit conversion, the two arguments that \lstinline$move_by()$ receives are pointers to
-\lstinline$cp1$'s second member and \lstinline$cp2$'s second member.
+Thanks to implicit conversion, the two arguments that \lstinline@move_by()@ receives are pointers to
+\lstinline@cp1@'s second member and \lstinline@cp2@'s second member.
 
 
@@ -467 +334 @@
 a direct safe arithmetic conversion;
 \item
-from any object type or incomplete type to \lstinline$void$;
-\item
-from a pointer to any non-\lstinline$void$ type to a pointer to \lstinline$void$;
+from any object type or incomplete type to \lstinline@void@;
+\item
+from a pointer to any non-\lstinline@void@ type to a pointer to \lstinline@void@;
 \item
 from a pointer to any type to a pointer to a more qualified version of the type\index{qualified type};
@@ -480 +347 @@
 Conversions that are not safe conversions are \define{unsafe conversion}s.
 \begin{rationale}
-As in C, there is an implicit conversion from \lstinline$void *$ to any pointer type.
+As in C, there is an implicit conversion from \lstinline@void *@ to any pointer type.
 This is clearly dangerous, and {\CC} does not have this implicit conversion.
 \CFA\index{deficiencies!void * conversion} keeps it, in the interest of remaining as pure a superset of C as possible, but discourages it by making it unsafe.
@@ -506 +373 @@
 \begin{itemize}
 \item
-The cost of an implicit conversion from \lstinline$int$ to \lstinline$long$ is 1.
-The cost of an implicit conversion from \lstinline$long$ to \lstinline$double$ is 3, because it is defined in terms of conversions from \lstinline$long$ to \lstinline$unsigned long$, then to \lstinline$float$, and then to \lstinline$double$.
-
-\item
-If \lstinline$int$ can represent all the values of \lstinline$unsigned short$, then the cost of an implicit conversion from \lstinline$unsigned short$ to \lstinline$unsigned$ is 2:
-\lstinline$unsigned short$ to \lstinline$int$ to \lstinline$unsigned$.
-Otherwise, \lstinline$unsigned short$ is converted directly to \lstinline$unsigned$, and the cost is 1.
-
-\item
-If \lstinline$long$ can represent all the values of \lstinline$unsigned$, then the conversion cost of \lstinline$unsigned$ to \lstinline$long$ is 1.
+The cost of an implicit conversion from \lstinline@int@ to \lstinline@long@ is 1.
+The cost of an implicit conversion from \lstinline@long@ to \lstinline@double@ is 3, because it is defined in terms of conversions from \lstinline@long@ to \lstinline@unsigned long@, then to \lstinline@float@, and then to \lstinline@double@.
+
+\item
+If \lstinline@int@ can represent all the values of \lstinline@unsigned short@, then the cost of an implicit conversion from \lstinline@unsigned short@ to \lstinline@unsigned@ is 2:
+\lstinline@unsigned short@ to \lstinline@int@ to \lstinline@unsigned@.
+Otherwise, \lstinline@unsigned short@ is converted directly to \lstinline@unsigned@, and the cost is 1.
+
+\item
+If \lstinline@long@ can represent all the values of \lstinline@unsigned@, then the conversion cost of \lstinline@unsigned@ to \lstinline@long@ is 1.
 Otherwise, the conversion is an unsafe conversion, and its conversion cost is undefined.
 \end{itemize}
@@ -523 +390 @@
 \begin{syntax}
 \oldlhs{keyword}
-        \rhs \lstinline$forall$
-        \rhs \lstinline$lvalue$
-        \rhs \lstinline$trait$
-        \rhs \lstinline$dtype$
-        \rhs \lstinline$ftype$
-        \rhs \lstinline$type$
+        \rhs \lstinline@forall@
+        \rhs \lstinline@lvalue@
+        \rhs \lstinline@trait@
+        \rhs \lstinline@dtype@
+        \rhs \lstinline@ftype@
+        \rhs \lstinline@otype@
 \end{syntax}
 
@@ -535 +402 @@
 
 \CFA allows operator \Index{overloading} by associating operators with special function identifiers.
-Furthermore, the constants ``\lstinline$0$'' and ``\lstinline$1$'' have special status for many of C's data types (and for many programmer-defined data types as well), so \CFA treats them as overloadable identifiers.
+Furthermore, the constants ``\lstinline@0@'' and ``\lstinline@1@'' have special status for many of C's data types (and for many programmer-defined data types as well), so \CFA treats them as overloadable identifiers.
 Programmers can use these identifiers to declare functions and objects that implement operators and constants for their own types.
 
@@ -544 +411 @@
 \begin{syntax}
 \oldlhs{identifier}
-\rhs \lstinline$0$
-\rhs \lstinline$1$
+\rhs \lstinline@0@
+\rhs \lstinline@1@
 \end{syntax}
 
-\index{constant identifiers}\index{identifiers!for constants} The tokens ``\lstinline$0$''\impl{0} and ``\lstinline$1$''\impl{1} are identifiers.
+\index{constant identifiers}\index{identifiers!for constants} The tokens ``\lstinline@0@''\impl{0} and ``\lstinline@1@''\impl{1} are identifiers.
 No other tokens defined by the rules for integer constants are considered to be identifiers.
 \begin{rationale}
-Why ``\lstinline$0$'' and ``\lstinline$1$''? Those integers have special status in C.
+Why ``\lstinline@0@'' and ``\lstinline@1@''? Those integers have special status in C.
 All scalar types can be incremented and decremented, which is defined in terms of adding or subtracting 1.
-The operations ``\lstinline$&&$'', ``\lstinline$||$'', and ``\lstinline$!$'' can be applied to any scalar arguments, and are defined in terms of comparison against 0.
+The operations ``\lstinline@&&@'', ``\lstinline@||@'', and ``\lstinline@!@'' can be applied to any scalar arguments, and are defined in terms of comparison against 0.
 A \nonterm{constant-expression} that evaluates to 0 is effectively compatible with every pointer type.
 
 In C, the integer constants 0 and 1 suffice because the integer promotion rules can convert them to any arithmetic type, and the rules for pointer expressions treat constant expressions evaluating to 0 as a special case.
 However, user-defined arithmetic types often need the equivalent of a 1 or 0 for their functions or operators, polymorphic functions often need 0 and 1 constants of a type matching their polymorphic parameters, and user-defined pointer-like types may need a null value.
-Defining special constants for a user-defined type is more efficient than defining a conversion to the type from \lstinline$_Bool$.
-
-Why \emph{just} ``\lstinline$0$'' and ``\lstinline$1$''? Why not other integers? No other integers have special status in C.
-A facility that let programmers declare specific constants---``\lstinline$const Rational 12$'', for instance---would not be much of an improvement.
+Defining special constants for a user-defined type is more efficient than defining a conversion to the type from \lstinline@_Bool@.
+
+Why \emph{just} ``\lstinline@0@'' and ``\lstinline@1@''? Why not other integers? No other integers have special status in C.
+A facility that let programmers declare specific constants---``\lstinline@const Rational 12@'', for instance---would not be much of an improvement.
 Some facility for defining the creation of values of programmer-defined types from arbitrary integer tokens would be needed.
 The complexity of such a feature doesn't seem worth the gain.
@@ -577 +444 @@
 \begin{tabular}[t]{ll}
 %identifier & operation \\ \hline
-\lstinline$?[?]$ & subscripting \impl{?[?]}\\
-\lstinline$?()$ & function call \impl{?()}\\
-\lstinline$?++$ & postfix increment \impl{?++}\\
-\lstinline$?--$ & postfix decrement \impl{?--}\\
-\lstinline$++?$ & prefix increment \impl{++?}\\
-\lstinline$--?$ & prefix decrement \impl{--?}\\
-\lstinline$*?$ & dereference \impl{*?}\\
-\lstinline$+?$ & unary plus \impl{+?}\\
-\lstinline$-?$ & arithmetic negation \impl{-?}\\
-\lstinline$~?$ & bitwise negation \impl{~?}\\
-\lstinline$!?$ & logical complement \impl{"!?}\\
-\lstinline$?*?$ & multiplication \impl{?*?}\\
-\lstinline$?/?$ & division \impl{?/?}\\
+\lstinline@?[?]@ & subscripting \impl{?[?]}\\
+\lstinline@?()@ & function call \impl{?()}\\
+\lstinline@?++@ & postfix increment \impl{?++}\\
+\lstinline@?--@ & postfix decrement \impl{?--}\\
+\lstinline@++?@ & prefix increment \impl{++?}\\
+\lstinline@--?@ & prefix decrement \impl{--?}\\
+\lstinline@*?@ & dereference \impl{*?}\\
+\lstinline@+?@ & unary plus \impl{+?}\\
+\lstinline@-?@ & arithmetic negation \impl{-?}\\
+\lstinline@~?@ & bitwise negation \impl{~?}\\
+\lstinline@!?@ & logical complement \impl{"!?}\\
+\lstinline@?*?@ & multiplication \impl{?*?}\\
+\lstinline@?/?@ & division \impl{?/?}\\
 \end{tabular}\hfil
 \begin{tabular}[t]{ll}
 %identifier & operation \\ \hline
-\lstinline$?%?$ & remainder \impl{?%?}\\
-\lstinline$?+?$ & addition \impl{?+?}\\
-\lstinline$?-?$ & subtraction \impl{?-?}\\
-\lstinline$?<<?$ & left shift \impl{?<<?}\\
-\lstinline$?>>?$ & right shift \impl{?>>?}\\
-\lstinline$?<?$ & less than \impl{?<?}\\
-\lstinline$?<=?$ & less than or equal \impl{?<=?}\\
-\lstinline$?>=?$ & greater than or equal \impl{?>=?}\\
-\lstinline$?>?$ & greater than \impl{?>?}\\
-\lstinline$?==?$ & equality \impl{?==?}\\
-\lstinline$?!=?$ & inequality \impl{?"!=?}\\
-\lstinline$?&?$ & bitwise AND \impl{?&?}\\
+\lstinline@?%?@ & remainder \impl{?%?}\\
+\lstinline@?+?@ & addition \impl{?+?}\\
+\lstinline@?-?@ & subtraction \impl{?-?}\\
+\lstinline@?<<?@ & left shift \impl{?<<?}\\
+\lstinline@?>>?@ & right shift \impl{?>>?}\\
+\lstinline@?<?@ & less than \impl{?<?}\\
+\lstinline@?<=?@ & less than or equal \impl{?<=?}\\
+\lstinline@?>=?@ & greater than or equal \impl{?>=?}\\
+\lstinline@?>?@ & greater than \impl{?>?}\\
+\lstinline@?==?@ & equality \impl{?==?}\\
+\lstinline@?!=?@ & inequality \impl{?"!=?}\\
+\lstinline@?&?@ & bitwise AND \impl{?&?}\\
 \end{tabular}\hfil
 \begin{tabular}[t]{ll}
 %identifier & operation \\ \hline
-\lstinline$?^?$ & exclusive OR \impl{?^?}\\
-\lstinline$?|?$ & inclusive OR \impl{?"|?}\\
-\lstinline$?=?$ & simple assignment \impl{?=?}\\
-\lstinline$?*=?$ & multiplication assignment \impl{?*=?}\\
-\lstinline$?/=?$ & division assignment \impl{?/=?}\\
-\lstinline$?%=?$ & remainder assignment \impl{?%=?}\\
-\lstinline$?+=?$ & addition assignment \impl{?+=?}\\
-\lstinline$?-=?$ & subtraction assignment \impl{?-=?}\\
-\lstinline$?<<=?$ & left-shift assignment \impl{?<<=?}\\
-\lstinline$?>>=?$ & right-shift assignment \impl{?>>=?}\\
-\lstinline$?&=?$ & bitwise AND assignment \impl{?&=?}\\
-\lstinline$?^=?$ & exclusive OR assignment \impl{?^=?}\\
-\lstinline$?|=?$ & inclusive OR assignment \impl{?"|=?}\\
+\lstinline@?^?@ & exclusive OR \impl{?^?}\\
+\lstinline@?|?@ & inclusive OR \impl{?"|?}\\
+\lstinline@?=?@ & simple assignment \impl{?=?}\\
+\lstinline@?*=?@ & multiplication assignment \impl{?*=?}\\
+\lstinline@?/=?@ & division assignment \impl{?/=?}\\
+\lstinline@?%=?@ & remainder assignment \impl{?%=?}\\
+\lstinline@?+=?@ & addition assignment \impl{?+=?}\\
+\lstinline@?-=?@ & subtraction assignment \impl{?-=?}\\
+\lstinline@?<<=?@ & left-shift assignment \impl{?<<=?}\\
+\lstinline@?>>=?@ & right-shift assignment \impl{?>>=?}\\
+\lstinline@?&=?@ & bitwise AND assignment \impl{?&=?}\\
+\lstinline@?^=?@ & exclusive OR assignment \impl{?^=?}\\
+\lstinline@?|=?@ & inclusive OR assignment \impl{?"|=?}\\
 \end{tabular}
 \hfil
@@ -635 +502 @@
 
 \begin{rationale}
-The use of ``\lstinline$?$'' in identifiers means that some C programs are not \CFA programs.  For instance, the sequence of characters ``\lstinline$(i < 0)?--i:i$'' is legal in a C program, but a
-\CFA compiler detects a syntax error because it treats ``\lstinline$?--$'' as an identifier, not as the two tokens ``\lstinline$?$'' and ``\lstinline$--$''.
+The use of ``\lstinline@?@'' in identifiers means that some C programs are not \CFA programs.  For instance, the sequence of characters ``\lstinline@(i < 0)?--i:i@'' is legal in a C program, but a
+\CFA compiler detects a syntax error because it treats ``\lstinline@?--@'' as an identifier, not as the two tokens ``\lstinline@?@'' and ``\lstinline@--@''.
 \end{rationale}
 
@@ -643 +510 @@
 \begin{itemize}
 \item
-The logical operators ``\lstinline$&&$'' and ``\lstinline$||$'', and the conditional operator
-``\lstinline$?:$''.
+The logical operators ``\lstinline@&&@'' and ``\lstinline@||@'', and the conditional operator
+``\lstinline@?:@''.
 These operators do not always evaluate their operands, and hence can not be properly defined by functions unless some mechanism like call-by-name is added to the language.
-Note that the definitions of ``\lstinline$&&$'' and ``\lstinline$||$'' say that they work by checking that their arguments are unequal to 0, so defining ``\lstinline$!=$'' and ``\lstinline$0$'' for user-defined types is enough to allow them to be used in logical expressions.
+Note that the definitions of ``\lstinline@&&@'' and ``\lstinline@||@'' say that they work by checking that their arguments are unequal to 0, so defining ``\lstinline@!=@'' and ``\lstinline@0@'' for user-defined types is enough to allow them to be used in logical expressions.
 
 \item
@@ -655 +522 @@
 \item
 The ``address of'' operator.
-It would seem useful to define a unary ``\lstinline$&$'' operator that returns values of some programmer-defined pointer-like type.
+It would seem useful to define a unary ``\lstinline@&@'' operator that returns values of some programmer-defined pointer-like type.
 The problem lies with the type of the operator.
-Consider the expression ``\lstinline$p = &x$'', where \lstinline$x$ is of type
-\lstinline$T$ and \lstinline$p$ has the programmer-defined type \lstinline$T_ptr$.
-The expression might be treated as a call to the unary function ``\lstinline$&?$''.
-Now what is the type of the function's parameter? It can not be \lstinline$T$, because then \lstinline$x$ would be passed by value, and there is no way to create a useful pointer-like result from a value.
-Hence the parameter must have type \lstinline$T *$.
-But then the expression must be rewritten as ``\lstinline$p = &?( &x )$''
+Consider the expression ``\lstinline@p = &x@'', where \lstinline@x@ is of type
+\lstinline@T@ and \lstinline@p@ has the programmer-defined type \lstinline@T_ptr@.
+The expression might be treated as a call to the unary function ``\lstinline@&?@''.
+Now what is the type of the function's parameter? It can not be \lstinline@T@, because then \lstinline@x@ would be passed by value, and there is no way to create a useful pointer-like result from a value.
+Hence the parameter must have type \lstinline@T *@.
+But then the expression must be rewritten as ``\lstinline@p = &?( &x )@''
 ---which doesn't seem like progress!
 
 The rule for address-of expressions would have to be something like ``keep applying address-of functions until you get one that takes a pointer argument, then use the built-in operator and stop''.
-It seems simpler to define a conversion function from \lstinline$T *$ to \lstinline$T_ptr$.
-
-\item
-The \lstinline$sizeof$ operator.
+It seems simpler to define a conversion function from \lstinline@T *@ to \lstinline@T_ptr@.
+
+\item
+The \lstinline@sizeof@ operator.
 It is already defined for every object type, and intimately tied into the language's storage allocation model.
 Redefining it seems pointless.
 
 \item
-The ``member of'' operators ``\lstinline$.$'' and ``\lstinline$->$''.
+The ``member of'' operators ``\lstinline@.@'' and ``\lstinline@->@''.
 These are not really infix operators, since their right ``operand'' is not a value or object.
 
@@ -711 +578 @@
 The ``fewest unsafe conversions'' rule ensures that the usual conversions are done, if possible.
 The ``lowest total expression cost'' rule chooses the proper common type.
-The odd-looking ``highest argument conversion cost'' rule ensures that, when unary expressions must be converted, conversions of function results are preferred to conversion of function arguments: \lstinline$(double)-i$ will be preferred to \lstinline$-(double)i$.
+The odd-looking ``highest argument conversion cost'' rule ensures that, when unary expressions must be converted, conversions of function results are preferred to conversion of function arguments: \lstinline@(double)-i@ will be preferred to \lstinline@-(double)i@.
 
 The ``least polymorphic'' rule reduces the number of polymorphic function calls, since such functions are presumably more expensive than monomorphic functions and since the more specific function is presumably more appropriate.
 It also gives preference to monomorphic values (such as the
-\lstinline$int$ \lstinline$0$) over polymorphic values (such as the \Index{null pointer}
-\lstinline$0$\use{0}).
+\lstinline@int@ \lstinline@0@) over polymorphic values (such as the \Index{null pointer}
+\lstinline@0@\use{0}).
 However, interpretations that call polymorphic functions are preferred to interpretations that perform unsafe conversions, because those conversions potentially lose accuracy or violate strong typing.
 
 There are two notable differences between \CFA's overload resolution rules and the rules for
-{\CC} defined in \cite{c++}.
+{\CC} defined in \cite{C++}.
 First, the result type of a function plays a role.
 In {\CC}, a function call must be completely resolved based on the arguments to the call in most circumstances.
@@ -736 +603 @@
 \begin{rationale}
 Predefined functions and constants have internal linkage because that simplifies optimization in traditional compile-and-link environments.
-For instance, ``\lstinline$an_int + an_int$'' is equivalent to ``\lstinline$?+?(an_int, an_int)$''.
+For instance, ``\lstinline@an_int + an_int@'' is equivalent to ``\lstinline@?+?(an_int, an_int)@''.
 If integer addition has not been redefined in the current scope, a compiler can generate code to perform the addition directly.
 If predefined functions had external linkage, this optimization would be difficult.
@@ -762 +629 @@
 \rhs \nonterm{constant}
 \rhs \nonterm{string-literal}
-\rhs \lstinline$($ \nonterm{expression} \lstinline$)$
+\rhs \lstinline@(@ \nonterm{expression} \lstinline@)@
 \rhs \nonterm{generic-selection}
 \end{syntax}
@@ -768 +635 @@
 \predefined
 \begin{lstlisting}
-const int 1;@\use{1}@
-const int 0;@\use{0}@
+const int 1;§\use{1}§
+const int 0;§\use{0}§
 forall( dtype DT ) DT * const 0;
 forall( ftype FT ) FT * const 0;
@@ -778 +645 @@
 
 A \nonterm{constant} or \nonterm{string-literal} has one valid interpretation, which has the type and value defined by {\c11}.
-The predefined integer identifiers ``\lstinline$1$'' and ``\lstinline$0$'' have the integer values 1 and 0, respectively.
-The other two predefined ``\lstinline$0$'' identifiers are bound to polymorphic pointer values that, when specialized\index{specialization} with a data type or function type respectively, produce a null pointer of that type.
+The predefined integer identifiers ``\lstinline@1@'' and ``\lstinline@0@'' have the integer values 1 and 0, respectively.
+The other two predefined ``\lstinline@0@'' identifiers are bound to polymorphic pointer values that, when specialized\index{specialization} with a data type or function type respectively, produce a null pointer of that type.
 
 A parenthesised expression has the same interpretations as the contained \nonterm{expression}.
 
 \examples
-The expression \lstinline$(void *)0$\use{0} specializes the (polymorphic) null pointer to a null pointer to \lstinline$void$. \lstinline$(const void *)0$ does the same, and also uses a safe conversion from \lstinline$void *$ to \lstinline$const void *$.
+The expression \lstinline@(void *)0@\use{0} specializes the (polymorphic) null pointer to a null pointer to \lstinline@void@. \lstinline@(const void *)0@ does the same, and also uses a safe conversion from \lstinline@void *@ to \lstinline@const void *@.
 In each case, the null pointer conversion is better\index{best valid interpretations} than the unsafe conversion of the integer
-\lstinline$0$ to a pointer.
+\lstinline@0@ to a pointer.
 
 \begin{rationale}
@@ -792 +659 @@
 
 \CFA does not have C's concept of ``null pointer constants'', which are not typed values but special strings of tokens.
-The C token ``\lstinline$0$'' is an expression of type \lstinline$int$ with the value ``zero'', and it \emph{also} is a null pointer constant.
+The C token ``\lstinline@0@'' is an expression of type \lstinline@int@ with the value ``zero'', and it \emph{also} is a null pointer constant.
 Similarly,
-``\lstinline$(void *)0$ is an expression of type \lstinline$(void *)$ whose value is a null pointer, and it also is a null pointer constant.
-However, in C, ``\lstinline$(void *)(void *)0$'' is
+``\lstinline@(void *)0@ is an expression of type \lstinline@(void *)@ whose value is a null pointer, and it also is a null pointer constant.
+However, in C, ``\lstinline@(void *)(void *)0@'' is
 \emph{not} a null pointer constant, even though it is null-valued, a pointer, and constant! The semantics of C expressions contain many special cases to deal with subexpressions that are null pointer constants.
 
@@ -802 +669 @@
 \begin{lstlisting}
 forall( dtype DT ) DT * const 0;
-\end{lstlisting} means that \lstinline$0$ is a polymorphic object, and contains a value that can have \emph{any} pointer-to-object type or pointer-to-incomplete type.
+\end{lstlisting} means that \lstinline@0@ is a polymorphic object, and contains a value that can have \emph{any} pointer-to-object type or pointer-to-incomplete type.
 The only such value is the null pointer.
 Therefore the type \emph{alone} is enough to identify a null pointer.
@@ -812 +679 @@
 
 \constraints The best interpretation of the controlling expression shall be unambiguous\index{ambiguous interpretation}, and shall have type compatible with at most one of the types named in its generic association list.
-If a generic selection has no \lstinline$default$ generic association, the best interpretation of its controlling expression shall have type compatible with exactly one of the types named in its generic association list.
+If a generic selection has no \lstinline@default@ generic association, the best interpretation of its controlling expression shall have type compatible with exactly one of the types named in its generic association list.
 
 \semantics
@@ -823 +690 @@
 \lhs{postfix-expression}
 \rhs \nonterm{primary-expression}
-\rhs \nonterm{postfix-expression} \lstinline$[$ \nonterm{expression} \lstinline$]$
-\rhs \nonterm{postfix-expression} \lstinline$($ 
-         \nonterm{argument-expression-list}\opt \lstinline$)$
-\rhs \nonterm{postfix-expression} \lstinline$.$ \nonterm{identifier}
-\rhs \nonterm{postfix-expression} \lstinline$->$ \nonterm{identifier}
-\rhs \nonterm{postfix-expression} \lstinline$++$
-\rhs \nonterm{postfix-expression} \lstinline$--$
-\rhs \lstinline$($ \nonterm{type-name} \lstinline$)$ \lstinline${$ \nonterm{initializer-list} \lstinline$}$
-\rhs \lstinline$($ \nonterm{type-name} \lstinline$)$ \lstinline${$ \nonterm{initializer-list} \lstinline$,$ \lstinline$}$
+\rhs \nonterm{postfix-expression} \lstinline@[@ \nonterm{expression} \lstinline@]@
+\rhs \nonterm{postfix-expression} \lstinline@(@ 
+         \nonterm{argument-expression-list}\opt \lstinline@)@
+\rhs \nonterm{postfix-expression} \lstinline@.@ \nonterm{identifier}
+\rhs \nonterm{postfix-expression} \lstinline@->@ \nonterm{identifier}
+\rhs \nonterm{postfix-expression} \lstinline@++@
+\rhs \nonterm{postfix-expression} \lstinline@--@
+\rhs \lstinline@(@ \nonterm{type-name} \lstinline@)@ \lstinline@{@ \nonterm{initializer-list} \lstinline@}@
+\rhs \lstinline@(@ \nonterm{type-name} \lstinline@)@ \lstinline@{@ \nonterm{initializer-list} \lstinline@,@ \lstinline@}@
 \lhs{argument-expression-list}
 \rhs \nonterm{assignment-expression}
-\rhs \nonterm{argument-expression-list} \lstinline$,$
+\rhs \nonterm{argument-expression-list} \lstinline@,@
          \nonterm{assignment-expression}
 \end{syntax}
@@ -840 +707 @@
 \rewriterules
 \begin{lstlisting}
-a[b] @\rewrite@ ?[?]( b, a ) // if a has integer type@\use{?[?]}@
-a[b] @\rewrite@ ?[?]( a, b ) // otherwise
-a( @\emph{arguments}@ ) @\rewrite@ ?()( a, @\emph{arguments}@ )@\use{?()}@
-a++ @\rewrite@ ?++(&( a ))@\use{?++}@
-a-- @\rewrite@ ?--(&( a ))@\use{?--}@
+a[b] §\rewrite§ ?[?]( b, a ) // if a has integer type§\use{?[?]}§
+a[b] §\rewrite§ ?[?]( a, b ) // otherwise
+a( §\emph{arguments}§ ) §\rewrite§ ?()( a, §\emph{arguments}§ )§\use{?()}§
+a++ §\rewrite§ ?++(&( a ))§\use{?++}§
+a-- §\rewrite§ ?--(&( a ))§\use{?--}§
 \end{lstlisting}
 
@@ -852 +719 @@
 \predefined
 \begin{lstlisting}
-forall( otype T ) lvalue T ?[?]( T *, ptrdiff_t );@\use{ptrdiff_t}@
+forall( otype T ) lvalue T ?[?]( T *, ptrdiff_t );§\use{ptrdiff_t}§
 forall( otype T ) lvalue _Atomic T ?[?]( _Atomic T *, ptrdiff_t );
 forall( otype T ) lvalue const T ?[?]( const T *, ptrdiff_t );
@@ -872 +739 @@
 The interpretations of subscript expressions are the interpretations of the corresponding function call expressions.
 \begin{rationale}
-C defines subscripting as pointer arithmetic in a way that makes \lstinline$a[i]$ and
-\lstinline$i[a]$ equivalent. \CFA provides the equivalence through a rewrite rule to reduce the number of overloadings of \lstinline$?[?]$.
+C defines subscripting as pointer arithmetic in a way that makes \lstinline@a[i]@ and
+\lstinline@i[a]@ equivalent. \CFA provides the equivalence through a rewrite rule to reduce the number of overloadings of \lstinline@?[?]@.
 
 Subscript expressions are rewritten as function calls that pass the first parameter by value.
 This is somewhat unfortunate, since array-like types tend to be large.
-The alternative is to use the rewrite rule ``\lstinline$a[b]$ \rewrite \lstinline$?[?](&(a), b)$''.
-However, C semantics forbid this approach: the \lstinline$a$ in ``\lstinline$a[b]$'' can be an arbitrary pointer value, which does not have an address.
+The alternative is to use the rewrite rule ``\lstinline@a[b]@ \rewrite \lstinline@?[?](&(a), b)@''.
+However, C semantics forbid this approach: the \lstinline@a@ in ``\lstinline@a[b]@'' can be an arbitrary pointer value, which does not have an address.
 
 The repetitive form of the predefined identifiers shows up a deficiency\index{deficiencies!pointers
@@ -893 +760 @@
 \nonterm{postfix-expression} in a function call may have some interpretations that are function designators and some that are not.
 
-For those interpretations of the \nonterm{postfix-expression} that are not function designators, the expression is rewritten and becomes a call of a function named ``\lstinline$?()$''.
+For those interpretations of the \nonterm{postfix-expression} that are not function designators, the expression is rewritten and becomes a call of a function named ``\lstinline@?()@''.
 The valid interpretations of the rewritten expression are determined in the manner described below.
 
@@ -901 +768 @@
 \item if the argument corresponds to a parameter in the function designator's prototype, the argument interpretation must have the same type as the corresponding parameter, or be implicitly convertible to the parameter's type
 \item if the function designator's type does not include a prototype or if the argument corresponds to
-``\lstinline$...$'' in a prototype, a \Index{default argument promotion} is applied to it.
+``\lstinline@...@'' in a prototype, a \Index{default argument promotion} is applied to it.
 \end{itemize}
 The type of the valid interpretation is the return type of the function designator.
@@ -909 +776 @@
 \begin{itemize}
 \item
-If the declaration of the implicit parameter uses \Index{type-class} \lstinline$type$\use{type}, the implicit argument must be an object type;
-if it uses \lstinline$dtype$, the implicit argument must be an object type or an incomplete type;
-and if it uses \lstinline$ftype$, the implicit argument must be a function type.
+If the declaration of the implicit parameter uses \Index{type-class} \lstinline@type@\use{type}, the implicit argument must be an object type;
+if it uses \lstinline@dtype@, the implicit argument must be an object type or an incomplete type;
+and if it uses \lstinline@ftype@, the implicit argument must be a function type.
 
 \item if an explicit parameter's type uses any implicit parameters, then the corresponding explicit argument must have a type that is (or can be safely converted\index{safe conversion} to) the type produced by substituting the implicit arguments for the implicit parameters in the explicit parameter type.
@@ -930 +797 @@
 \begin{rationale}
 One desirable property of a polymorphic programming language is \define{generalizability}: the ability to replace an abstraction with a more general but equivalent abstraction without requiring changes in any of the uses of the original\cite{Cormack90}.
-For instance, it should be possible to replace a function ``\lstinline$int f( int );$'' with ``\lstinline$forall( otype T ) T f( T );$'' without affecting any calls of \lstinline$f$.
+For instance, it should be possible to replace a function ``\lstinline@int f( int );@'' with ``\lstinline@forall( otype T ) T f( T );@'' without affecting any calls of \lstinline@f@.
 
 \CFA\index{deficiencies!generalizability} does not fully possess this property, because
@@ -944 +811 @@
 f = g( d, f );          // (3) (unsafe conversion to float) 
 \end{lstlisting}
-If \lstinline$g$ was replaced by ``\lstinline$forall( otype T ) T g( T, T );$'', the first and second calls would be unaffected, but the third would change: \lstinline$f$ would be converted to
-\lstinline$double$, and the result would be a \lstinline$double$.
-
-Another example is the function ``\lstinline$void h( int *);$''.
+If \lstinline@g@ was replaced by ``\lstinline@forall( otype T ) T g( T, T );@'', the first and second calls would be unaffected, but the third would change: \lstinline@f@ would be converted to
+\lstinline@double@, and the result would be a \lstinline@double@.
+
+Another example is the function ``\lstinline@void h( int *);@''.
 This function can be passed a
-\lstinline$void *$ argument, but the generalization ``\lstinline$forall( otype T ) void h( T *);$'' can not.
-In this case, \lstinline$void$ is not a valid value for \lstinline$T$ because it is not an object type.
-If unsafe conversions were allowed, \lstinline$T$ could be inferred to be \emph{any} object type, which is undesirable.
+\lstinline@void *@ argument, but the generalization ``\lstinline@forall( otype T ) void h( T *);@'' can not.
+In this case, \lstinline@void@ is not a valid value for \lstinline@T@ because it is not an object type.
+If unsafe conversions were allowed, \lstinline@T@ could be inferred to be \emph{any} object type, which is undesirable.
 \end{rationale}
 
 \examples
-A function called ``\lstinline$?()$'' might be part of a numerical differentiation package.
+A function called ``\lstinline@?()@'' might be part of a numerical differentiation package.
 \begin{lstlisting}
 extern otype Derivative;
@@ -966 +833 @@
 d = sin_dx( 12.9 );
 \end{lstlisting}
-Here, the only interpretation of \lstinline$sin_dx$ is as an object of type \lstinline$Derivative$.
-For that interpretation, the function call is treated as ``\lstinline$?()( sin_dx, 12.9 )$''.
+Here, the only interpretation of \lstinline@sin_dx@ is as an object of type \lstinline@Derivative@.
+For that interpretation, the function call is treated as ``\lstinline@?()( sin_dx, 12.9 )@''.
 \begin{lstlisting}
 int f( long );          // (1)
@@ -974 +841 @@
 int i = f( 5 );         // calls (1) 
 \end{lstlisting}
-Function (1) provides a valid interpretation of ``\lstinline$f( 5 )$'', using an implicit \lstinline$int$ to \lstinline$long$ conversion.
-The other functions do not, since the second requires two arguments, and since there is no implicit conversion from \lstinline$int$ to \lstinline$int *$ that could be used with the third function.
+Function (1) provides a valid interpretation of ``\lstinline@f( 5 )@'', using an implicit \lstinline@int@ to \lstinline@long@ conversion.
+The other functions do not, since the second requires two arguments, and since there is no implicit conversion from \lstinline@int@ to \lstinline@int *@ that could be used with the third function.
 
 \begin{lstlisting}
@@ -981 +848 @@
 double d = h( 1.5 );
 \end{lstlisting}
-``\lstinline$1.5$'' is a \lstinline$double$ constant, so \lstinline$T$ is inferred to be
-\lstinline$double$, and the result of the function call is a \lstinline$double$.
+``\lstinline@1.5@'' is a \lstinline@double@ constant, so \lstinline@T@ is inferred to be
+\lstinline@double@, and the result of the function call is a \lstinline@double@.
 
 \begin{lstlisting}
@@ -997 +864 @@
 g( i, p );                      // calls (4) 
 \end{lstlisting}
-The first call has valid interpretations for all four versions of \lstinline$g$. (6) and (7) are discarded because they involve unsafe \lstinline$double$-to-\lstinline$long$ conversions. (5) is chosen because it is less polymorphic than (4).
+The first call has valid interpretations for all four versions of \lstinline@g@. (6) and (7) are discarded because they involve unsafe \lstinline@double@-to-\lstinline@long@ conversions. (5) is chosen because it is less polymorphic than (4).
 
 For the second call, (7) is again discarded.
-Of the remaining interpretations for (4), (5), and (6) (with \lstinline$i$ converted to \lstinline$long$), (6) is chosen because it is the least polymorphic.
+Of the remaining interpretations for (4), (5), and (6) (with \lstinline@i@ converted to \lstinline@long@), (6) is chosen because it is the least polymorphic.
 
 The third call has valid interpretations for all of the functions;
@@ -1009 +876 @@
 forall( otype T ) T min( T, T );
 double max( double, double );
-trait min_max( T ) {@\impl{min_max}@
+trait min_max( T ) {§\impl{min_max}§
         T min( T, T );
         T max( T, T );
@@ -1016 +883 @@
 shuffle( 9, 10 );
 \end{lstlisting}
-The only possibility for \lstinline$U$ is \lstinline$double$, because that is the type used in the only visible \lstinline$max$ function. 9 and 10 must be converted to \lstinline$double$, and
-\lstinline$min$ must be specialized with \lstinline$T$ bound to \lstinline$double$.
+The only possibility for \lstinline@U@ is \lstinline@double@, because that is the type used in the only visible \lstinline@max@ function. 9 and 10 must be converted to \lstinline@double@, and
+\lstinline@min@ must be specialized with \lstinline@T@ bound to \lstinline@double@.
 \begin{lstlisting}
 extern void q( int );           // (8)
@@ -1025 +892 @@
 r( 0 );
 \end{lstlisting}
-The \lstinline$int 0$ could be passed to (8), or the \lstinline$(void *)$ \Index{specialization} of the null pointer\index{null pointer} \lstinline$0$\use{0} could be passed to (9).
-The former is chosen because the \lstinline$int$ \lstinline$0$ is \Index{less polymorphic}.
-For the same reason, \lstinline$int$ \lstinline$0$ is passed to \lstinline$r()$, even though it has \emph{no} declared parameter types.
+The \lstinline@int 0@ could be passed to (8), or the \lstinline@(void *)@ \Index{specialization} of the null pointer\index{null pointer} \lstinline@0@\use{0} could be passed to (9).
+The former is chosen because the \lstinline@int@ \lstinline@0@ is \Index{less polymorphic}.
+For the same reason, \lstinline@int@ \lstinline@0@ is passed to \lstinline@r()@, even though it has \emph{no} declared parameter types.
 
 
 \subsubsection{Structure and union members}
 
-\semantics In the member selection expression ``\lstinline$s$.\lstinline$m$'', there shall be at least one interpretation of \lstinline$s$ whose type is a structure type or union type containing a member named \lstinline$m$.
-If two or more interpretations of \lstinline$s$ have members named
-\lstinline$m$ with mutually compatible types, then the expression has an \Index{ambiguous interpretation} whose type is the composite type of the types of the members.
-If an interpretation of \lstinline$s$ has a member \lstinline$m$ whose type is not compatible with any other
-\lstinline$s$'s \lstinline$m$, then the expression has an interpretation with the member's type.
+\semantics In the member selection expression ``\lstinline@s@.\lstinline@m@'', there shall be at least one interpretation of \lstinline@s@ whose type is a structure type or union type containing a member named \lstinline@m@.
+If two or more interpretations of \lstinline@s@ have members named
+\lstinline@m@ with mutually compatible types, then the expression has an \Index{ambiguous interpretation} whose type is the composite type of the types of the members.
+If an interpretation of \lstinline@s@ has a member \lstinline@m@ whose type is not compatible with any other
+\lstinline@s@'s \lstinline@m@, then the expression has an interpretation with the member's type.
 The expression has no other interpretations.
 
-The expression ``\lstinline$p->m$'' has the same interpretations as the expression
-``\lstinline$(*p).m$''.
+The expression ``\lstinline@p->m@'' has the same interpretations as the expression ``\lstinline@(*p).m@''.
 
 
@@ -1135 +1001 @@
         * ?--( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ there exist
+For every extended integer type \lstinline@X@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1141 +1007 @@
   ?--( volatile X * ), ?--( _Atomic volatile X * );
 \end{lstlisting}
-For every complete enumerated type \lstinline$E$ there exist
+For every complete enumerated type \lstinline@E@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1149 +1015 @@
 
 \begin{rationale}
-Note that ``\lstinline$++$'' and ``\lstinline$--$'' are rewritten as function calls that are given a pointer to that operand. (This is true of all operators that modify an operand.) As Hamish Macdonald has pointed out, this forces the modified operand of such expressions to be an lvalue.
+Note that ``\lstinline@++@'' and ``\lstinline@--@'' are rewritten as function calls that are given a pointer to that operand. (This is true of all operators that modify an operand.) As Hamish Macdonald has pointed out, this forces the modified operand of such expressions to be an lvalue.
 This partially enforces the C semantic rule that such operands must be \emph{modifiable} lvalues.
 \end{rationale}
@@ -1155 +1021 @@
 \begin{rationale}
 In C, a semantic rule requires that pointer operands of increment and decrement be pointers to object types.
-Hence, \lstinline$void *$ objects cannot be incremented.
-In \CFA, the restriction follows from the use of a \lstinline$type$ parameter in the predefined function definitions, as opposed to \lstinline$dtype$, since only object types can be inferred arguments corresponding to the type parameter \lstinline$T$.
+Hence, \lstinline@void *@ objects cannot be incremented.
+In \CFA, the restriction follows from the use of a \lstinline@type@ parameter in the predefined function definitions, as opposed to \lstinline@dtype@, since only object types can be inferred arguments corresponding to the type parameter \lstinline@T@.
 \end{rationale}
 
 \semantics
 First, each interpretation of the operand of an increment or decrement expression is considered separately.
-For each interpretation that is a bit-field or is declared with the
-\lstinline$register$\index{register@{\lstinline$register$}} \index{Itorage-class specifier}, the expression has one valid interpretation, with the type of the operand, and the expression is ambiguous if the operand is.
+For each interpretation that is a bit-field or is declared with the \Indexc{register}\index{storage-class specifier}, the expression has one valid interpretation, with the type of the operand, and the expression is ambiguous if the operand is.
 
 For the remaining interpretations, the expression is rewritten, and the interpretations of the expression are the interpretations of the corresponding function call.
@@ -1175 +1040 @@
 \end{lstlisting}
 \begin{sloppypar}
-Since \lstinline$&(vs)$ has type \lstinline$volatile short int *$, the best valid interpretation of
-\lstinline$vs++$ calls the \lstinline$?++$ function with the \lstinline$volatile short *$ parameter.
-\lstinline$s++$ does the same, applying the safe conversion from \lstinline$short int *$ to
-\lstinline$volatile short int *$.
-Note that there is no conversion that adds an \lstinline$_Atomic$ qualifier, so the \lstinline$_Atomic volatile short int$ overloading does not provide a valid interpretation.
+Since \lstinline@&(vs)@ has type \lstinline@volatile short int *@, the best valid interpretation of
+\lstinline@vs++@ calls the \lstinline@?++@ function with the \lstinline@volatile short *@ parameter.
+\lstinline@s++@ does the same, applying the safe conversion from \lstinline@short int *@ to \lstinline@volatile short int *@.
+Note that there is no conversion that adds an \lstinline@_Atomic@ qualifier, so the \lstinline@_Atomic volatile short int@ overloading does not provide a valid interpretation.
 \end{sloppypar}
 
-There is no safe conversion from \lstinline$const short int *$ to \lstinline$volatile short int *$, and no \lstinline$?++$ function that accepts a \lstinline$const *$ parameter, so \lstinline$cs++$ has no valid interpretations.
-
-The best valid interpretation of \lstinline$as++$ calls the \lstinline$short ?++$ function with the \lstinline$_Atomic volatile short int *$ parameter, applying a safe conversion to add the \lstinline$volatile$ qualifier.
+There is no safe conversion from \lstinline@const short int *@ to \lstinline@volatile short int *@, and no \lstinline@?++@ function that accepts a \lstinline@const *@ parameter, so \lstinline@cs++@ has no valid interpretations.
+
+The best valid interpretation of \lstinline@as++@ calls the \lstinline@short ?++@ function with the \lstinline@_Atomic volatile short int *@ parameter, applying a safe conversion to add the \lstinline@volatile@ qualifier.
 \begin{lstlisting}
 char * const restrict volatile * restrict volatile pqpc;
@@ -1191 +1055 @@
 ppc++;
 \end{lstlisting}
-Since \lstinline$&(pqpc)$ has type \lstinline$char * const restrict volatile * restrict volatile *$, the best valid interpretation of \lstinline$pqpc++$ calls the polymorphic \lstinline$?++$ function with the \lstinline$const restrict volatile T * restrict volatile *$ parameter, inferring \lstinline$T$ to be \lstinline$char *$.
-
-\lstinline$ppc++$ calls the same function, again inferring \lstinline$T$ to be \lstinline$char *$, and using the safe conversions from \lstinline$T$ to \lstinline$T const$ \lstinline$restrict volatile$.
+Since \lstinline@&(pqpc)@ has type \lstinline@char * const restrict volatile * restrict volatile *@, the best valid interpretation of \lstinline@pqpc++@ calls the polymorphic \lstinline@?++@ function with the \lstinline@const restrict volatile T * restrict volatile *@ parameter, inferring \lstinline@T@ to be \lstinline@char *@.
+
+\lstinline@ppc++@ calls the same function, again inferring \lstinline@T@ to be \lstinline@char *@, and using the safe conversions from \lstinline@T@ to \lstinline@T const@ \lstinline@restrict volatile@.
 
 \begin{rationale}
@@ -1207 +1071 @@
 \begin{enumerate}
 \item
-``\lstinline$char * p; p++;$''.
-The argument to \lstinline$?++$ has type \lstinline$char * *$, and the result has type \lstinline$char *$.
-The expression would be valid if \lstinline$?++$ were declared by
+``\lstinline@char * p; p++;@''.
+The argument to \lstinline@?++@ has type \lstinline@char * *@, and the result has type \lstinline@char *@.
+The expression would be valid if \lstinline@?++@ were declared by
 \begin{lstlisting}
 forall( otype T ) T * ?++( T * * );
-\end{lstlisting} with \lstinline$T$ inferred to be \lstinline$char$.
-
-\item
-``\lstinline$char *restrict volatile qp; qp++$''.
-The result again has type \lstinline$char *$, but the argument now has type \lstinline$char *restrict volatile *$, so it cannot be passed to the hypothetical function declared in point 1.
+\end{lstlisting} with \lstinline@T@ inferred to be \lstinline@char@.
+
+\item
+``\lstinline@char *restrict volatile qp; qp++@''.
+The result again has type \lstinline@char *@, but the argument now has type \lstinline@char *restrict volatile *@, so it cannot be passed to the hypothetical function declared in point 1.
 Hence the actual predefined function is
 \begin{lstlisting}
 forall( otype T ) T * ?++( T * restrict volatile * );
-\end{lstlisting} which also accepts a \lstinline$char * *$ argument, because of the safe conversions that add
-\lstinline$volatile$ and \lstinline$restrict$ qualifiers. (The parameter is not const-qualified, so constant pointers cannot be incremented.)
-
-\item
-``\lstinline$char *_Atomic ap; ap++$''.
-The result again has type \lstinline$char *$, but no safe conversion adds an \lstinline$_Atomic$ qualifier, so the function in point 2 is not applicable.
-A separate overloading of \lstinline$?++$ is required.
-
-\item
-``\lstinline$char const volatile * pq; pq++$''.
+\end{lstlisting} which also accepts a \lstinline@char * *@ argument, because of the safe conversions that add
+\lstinline@volatile@ and \lstinline@restrict@ qualifiers. (The parameter is not const-qualified, so constant pointers cannot be incremented.)
+
+\item
+``\lstinline@char *_Atomic ap; ap++@''.
+The result again has type \lstinline@char *@, but no safe conversion adds an \lstinline@_Atomic@ qualifier, so the function in point 2 is not applicable.
+A separate overloading of \lstinline@?++@ is required.
+
+\item
+``\lstinline@char const volatile * pq; pq++@''.
 Here the result has type
-\lstinline$char const volatile *$, so a new overloading is needed:
+\lstinline@char const volatile *@, so a new overloading is needed:
 \begin{lstlisting}
 forall( otype T ) T const volatile * ?++( T const volatile *restrict volatile * );
@@ -1238 +1102 @@
  
 \item
-``\lstinline$float *restrict * prp; prp++$''.
-The \lstinline$restrict$ qualifier is handled just like \lstinline$const$ and \lstinline$volatile$ in the previous case:
+``\lstinline@float *restrict * prp; prp++@''.
+The \lstinline@restrict@ qualifier is handled just like \lstinline@const@ and \lstinline@volatile@ in the previous case:
 \begin{lstlisting}
 forall( otype T ) T restrict * ?++( T restrict *restrict volatile * );
-\end{lstlisting} with \lstinline$T$ inferred to be \lstinline$float *$.
-This looks odd, because {\c11} contains a constraint that requires restrict-qualified types to be pointer-to-object types, and \lstinline$T$ is not syntactically a pointer type. \CFA loosens the constraint.
+\end{lstlisting} with \lstinline@T@ inferred to be \lstinline@float *@.
+This looks odd, because {\c11} contains a constraint that requires restrict-qualified types to be pointer-to-object types, and \lstinline@T@ is not syntactically a pointer type. \CFA loosens the constraint.
 \end{enumerate}
 \end{rationale}
@@ -1259 +1123 @@
 \lhs{unary-expression}
 \rhs \nonterm{postfix-expression}
-\rhs \lstinline$++$ \nonterm{unary-expression}
-\rhs \lstinline$--$ \nonterm{unary-expression}
+\rhs \lstinline@++@ \nonterm{unary-expression}
+\rhs \lstinline@--@ \nonterm{unary-expression}
 \rhs \nonterm{unary-operator} \nonterm{cast-expression}
-\rhs \lstinline$sizeof$ \nonterm{unary-expression}
-\rhs \lstinline$sizeof$ \lstinline$($ \nonterm{type-name} \lstinline$)$
-\lhs{unary-operator} one of \rhs \lstinline$&$ \lstinline$*$ \lstinline$+$ \lstinline$-$ \lstinline$~$ \lstinline$!$
+\rhs \lstinline@sizeof@ \nonterm{unary-expression}
+\rhs \lstinline@sizeof@ \lstinline@(@ \nonterm{type-name} \lstinline@)@
+\lhs{unary-operator} one of \rhs \lstinline@&@ \lstinline@*@ \lstinline@+@ \lstinline@-@ \lstinline@~@ \lstinline@!@
 \end{syntax}
 
 \rewriterules
 \begin{lstlisting}
-*a      @\rewrite@ *?( a ) @\use{*?}@
-+a      @\rewrite@ +?( a ) @\use{+?}@
--a      @\rewrite@ -?( a ) @\use{-?}@
-~a      @\rewrite@ ~?( a ) @\use{~?}@
-!a      @\rewrite@ !?( a ) @\use{"!?}@
-++a     @\rewrite@ ++?(&( a )) @\use{++?}@
---a     @\rewrite@ --?(&( a )) @\use{--?}@
+*a      §\rewrite§ *?( a ) §\use{*?}§
++a      §\rewrite§ +?( a ) §\use{+?}§
+-a      §\rewrite§ -?( a ) §\use{-?}§
+~a      §\rewrite§ ~?( a ) §\use{~?}§
+!a      §\rewrite§ !?( a ) §\use{"!?}§
+++a     §\rewrite§ ++?(&( a )) §\use{++?}§
+--a     §\rewrite§ --?(&( a )) §\use{--?}§
 \end{lstlisting}
 
@@ -1371 +1235 @@
         * --?( _Atomic const restrict volatile T * _Atomic restrict volatile * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ there exist
+For every extended integer type \lstinline@X@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1379 +1243 @@
         --?( _Atomic volatile X * );
 \end{lstlisting}
-For every complete enumerated type \lstinline$E$ there exist
+For every complete enumerated type \lstinline@E@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1416 +1280 @@
 
 \constraints
-The operand of the unary ``\lstinline$&$'' operator shall have exactly one
+The operand of the unary ``\lstinline@&@'' operator shall have exactly one
 \Index{interpretation}\index{ambiguous interpretation}, which shall be unambiguous.
 
 \semantics
-The ``\lstinline$&$'' expression has one interpretation which is of type \lstinline$T *$, where
-\lstinline$T$ is the type of the operand.
+The ``\lstinline@&@'' expression has one interpretation which is of type \lstinline@T *@, where
+\lstinline@T@ is the type of the operand.
 
 The interpretations of an indirection expression are the interpretations of the corresponding function call.
@@ -1450 +1314 @@
 forall( ftype FT ) int !?( FT * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1463 +1327 @@
 \begin{lstlisting}
 long int li;
-void eat_double( double );@\use{eat_double}@
-eat_double(-li ); // @\rewrite@ eat_double( -?( li ) );
-\end{lstlisting}
-The valid interpretations of ``\lstinline$-li$'' (assuming no extended integer types exist) are
+void eat_double( double );§\use{eat_double}§
+eat_double(-li ); // §\rewrite§ eat_double( -?( li ) );
+\end{lstlisting}
+The valid interpretations of ``\lstinline@-li@'' (assuming no extended integer types exist) are
 \begin{center}
 \begin{tabular}{llc} interpretation & result type & expression conversion cost \\
 \hline
-\lstinline$-?( (int)li )$                                       & \lstinline$int$                                       & (unsafe) \\
-\lstinline$-?( (unsigned)li)$                           & \lstinline$unsigned int$                      & (unsafe) \\
-\lstinline$-?( (long)li)$                                       & \lstinline$long$                                      & 0 \\
-\lstinline$-?( (long unsigned int)li)$          & \lstinline$long unsigned int$         & 1 \\
-\lstinline$-?( (long long int)li)$                      & \lstinline$long long int$                     & 2 \\
-\lstinline$-?( (long long unsigned int)li)$     & \lstinline$long long unsigned int$& 3 \\
-\lstinline$-?( (float)li)$                                      & \lstinline$float$                                     & 4 \\
-\lstinline$-?( (double)li)$                                     & \lstinline$double$                            & 5 \\
-\lstinline$-?( (long double)li)$                        & \lstinline$long double$                       & 6 \\
-\lstinline$-?( (_Complex float)li)$                     & \lstinline$float$                                     & (unsafe) \\
-\lstinline$-?( (_Complex double)li)$            & \lstinline$double$                            & (unsafe) \\
-\lstinline$-?( (_Complex long double)li)$       & \lstinline$long double$                       & (unsafe) \\
+\lstinline@-?( (int)li )@                                       & \lstinline@int@                                       & (unsafe) \\
+\lstinline@-?( (unsigned)li)@                           & \lstinline@unsigned int@                      & (unsafe) \\
+\lstinline@-?( (long)li)@                                       & \lstinline@long@                                      & 0 \\
+\lstinline@-?( (long unsigned int)li)@          & \lstinline@long unsigned int@         & 1 \\
+\lstinline@-?( (long long int)li)@                      & \lstinline@long long int@                     & 2 \\
+\lstinline@-?( (long long unsigned int)li)@     & \lstinline@long long unsigned int@& 3 \\
+\lstinline@-?( (float)li)@                                      & \lstinline@float@                                     & 4 \\
+\lstinline@-?( (double)li)@                                     & \lstinline@double@                            & 5 \\
+\lstinline@-?( (long double)li)@                        & \lstinline@long double@                       & 6 \\
+\lstinline@-?( (_Complex float)li)@                     & \lstinline@float@                                     & (unsafe) \\
+\lstinline@-?( (_Complex double)li)@            & \lstinline@double@                            & (unsafe) \\
+\lstinline@-?( (_Complex long double)li)@       & \lstinline@long double@                       & (unsafe) \\
 \end{tabular}
 \end{center}
-The valid interpretations of the \lstinline$eat_double$ call, with the cost of the argument conversion and the cost of the entire expression, are
+The valid interpretations of the \lstinline@eat_double@ call, with the cost of the argument conversion and the cost of the entire expression, are
 \begin{center}
 \begin{tabular}{lcc} interpretation & argument cost & expression cost \\
 \hline
-\lstinline$eat_double( (double)-?( (int)li) )$                                  & 7                     & (unsafe) \\
-\lstinline$eat_double( (double)-?( (unsigned)li) )$                             & 6                     & (unsafe) \\
-\lstinline$eat_double( (double)-?(li) )$                                                & 5                     & \(0+5=5\) \\
-\lstinline$eat_double( (double)-?( (long unsigned int)li) )$    & 4                     & \(1+4=5\) \\
-\lstinline$eat_double( (double)-?( (long long int)li) )$                & 3                     & \(2+3=5\) \\
-\lstinline$eat_double( (double)-?( (long long unsigned int)li) )$& 2            & \(3+2=5\) \\
-\lstinline$eat_double( (double)-?( (float)li) )$                                & 1                     & \(4+1=5\) \\
-\lstinline$eat_double( (double)-?( (double)li) )$                               & 0                     & \(5+0=5\) \\
-\lstinline$eat_double( (double)-?( (long double)li) )$                  & (unsafe)      & (unsafe) \\
-\lstinline$eat_double( (double)-?( (_Complex float)li) )$               & (unsafe)      & (unsafe) \\
-\lstinline$eat_double( (double)-?( (_Complex double)li) )$              & (unsafe)      & (unsafe) \\
-\lstinline$eat_double( (double)-?( (_Complex long double)li) )$ & (unsafe)      & (unsafe) \\
+\lstinline@eat_double( (double)-?( (int)li) )@                                  & 7                     & (unsafe) \\
+\lstinline@eat_double( (double)-?( (unsigned)li) )@                             & 6                     & (unsafe) \\
+\lstinline@eat_double( (double)-?(li) )@                                                & 5                     & \(0+5=5\) \\
+\lstinline@eat_double( (double)-?( (long unsigned int)li) )@    & 4                     & \(1+4=5\) \\
+\lstinline@eat_double( (double)-?( (long long int)li) )@                & 3                     & \(2+3=5\) \\
+\lstinline@eat_double( (double)-?( (long long unsigned int)li) )@& 2            & \(3+2=5\) \\
+\lstinline@eat_double( (double)-?( (float)li) )@                                & 1                     & \(4+1=5\) \\
+\lstinline@eat_double( (double)-?( (double)li) )@                               & 0                     & \(5+0=5\) \\
+\lstinline@eat_double( (double)-?( (long double)li) )@                  & (unsafe)      & (unsafe) \\
+\lstinline@eat_double( (double)-?( (_Complex float)li) )@               & (unsafe)      & (unsafe) \\
+\lstinline@eat_double( (double)-?( (_Complex double)li) )@              & (unsafe)      & (unsafe) \\
+\lstinline@eat_double( (double)-?( (_Complex long double)li) )@ & (unsafe)      & (unsafe) \\
 \end{tabular}
 \end{center}
-Each has result type \lstinline$void$, so the best must be selected.
+Each has result type \lstinline@void@, so the best must be selected.
 The interpretations involving unsafe conversions are discarded.
 The remainder have equal expression conversion costs, so the
 ``highest argument conversion cost'' rule is invoked, and the chosen interpretation is
-\lstinline$eat_double( (double)-?(li) )$.
-
-
-\subsubsection{The \lstinline$sizeof$ and \lstinline$_Alignof$ operators}
+\lstinline@eat_double( (double)-?(li) )@.
+
+
+\subsubsection[The sizeof and \_Alignof operators]{The \lstinline@sizeof@ and \lstinline@_Alignof@ operators}
 
 \constraints
-The operand of \lstinline$sizeof$ or \lstinline$_Alignof$ shall not be \lstinline$type$,
-\lstinline$dtype$, or \lstinline$ftype$.
-
-When the \lstinline$sizeof$\use{sizeof} operator is applied to an expression, the expression shall have exactly one \Index{interpretation}\index{ambiguous interpretation}, which shall be unambiguous. \semantics A \lstinline$sizeof$ or \lstinline$_Alignof$ expression has one interpretation, of type \lstinline$size_t$.
-
-When \lstinline$sizeof$ is applied to an identifier declared by a \nonterm{type-declaration} or a
+The operand of \lstinline@sizeof@ or \lstinline@_Alignof@ shall not be \lstinline@type@, \lstinline@dtype@, or \lstinline@ftype@.
+
+When the \lstinline@sizeof@\use{sizeof} operator is applied to an expression, the expression shall have exactly one \Index{interpretation}\index{ambiguous interpretation}, which shall be unambiguous. \semantics A \lstinline@sizeof@ or \lstinline@_Alignof@ expression has one interpretation, of type \lstinline@size_t@.
+
+When \lstinline@sizeof@ is applied to an identifier declared by a \nonterm{type-declaration} or a
 \nonterm{type-parameter}, it yields the size in bytes of the type that implements the operand.
 When the operand is an opaque type or an inferred type parameter\index{inferred parameter}, the expression is not a constant expression.
 
-When \lstinline$_Alignof$ is applied to an identifier declared by a \nonterm{type-declaration} or a
+When \lstinline@_Alignof@ is applied to an identifier declared by a \nonterm{type-declaration} or a
 \nonterm{type-parameter}, it yields the alignment requirement of the type that implements the operand.
 When the operand is an opaque type or an inferred type parameter\index{inferred parameter}, the expression is not a constant expression.
@@ -1528 +1391 @@
 otype Pair = struct { int first, second; };
 size_t p_size = sizeof(Pair);           // constant expression 
-extern otype Rational;@\use{Rational}@
+extern otype Rational;§\use{Rational}§
 size_t c_size = sizeof(Rational);       // non-constant expression 
 forall(type T) T f(T p1, T p2) {
@@ -1535 +1398 @@
 }
 \end{lstlisting}
-``\lstinline$sizeof Rational$'', although not statically known, is fixed.
-Within \lstinline$f()$,
-``\lstinline$sizeof(T)$'' is fixed for each call of \lstinline$f()$, but may vary from call to call.
+``\lstinline@sizeof Rational@'', although not statically known, is fixed.
+Within \lstinline@f()@,
+``\lstinline@sizeof(T)@'' is fixed for each call of \lstinline@f()@, but may vary from call to call.
 \end{rationale}
 
@@ -1546 +1409 @@
 \lhs{cast-expression}
 \rhs \nonterm{unary-expression}
-\rhs \lstinline$($ \nonterm{type-name} \lstinline$)$ \nonterm{cast-expression}
+\rhs \lstinline@(@ \nonterm{type-name} \lstinline@)@ \nonterm{cast-expression}
 \end{syntax}
 
 \constraints
-The \nonterm{type-name} in a \nonterm{cast-expression} shall not be \lstinline$type$,
-\lstinline$dtype$, or \lstinline$ftype$.
+The \nonterm{type-name} in a \nonterm{cast-expression} shall not be \lstinline@type@,
+\lstinline@dtype@, or \lstinline@ftype@.
 
 \semantics
 
-In a \Index{cast expression} ``\lstinline$($\nonterm{type-name}\lstinline$)e$'', if
-\nonterm{type-name} is the type of an interpretation of \lstinline$e$, then that interpretation is the only interpretation of the cast expression;
-otherwise, \lstinline$e$ shall have some interpretation that can be converted to \nonterm{type-name}, and the interpretation of the cast expression is the cast of the interpretation that can be converted at the lowest cost.
+In a \Index{cast expression} ``\lstinline@(@\nonterm{type-name}\lstinline@)e@'', if
+\nonterm{type-name} is the type of an interpretation of \lstinline@e@, then that interpretation is the only interpretation of the cast expression;
+otherwise, \lstinline@e@ shall have some interpretation that can be converted to \nonterm{type-name}, and the interpretation of the cast expression is the cast of the interpretation that can be converted at the lowest cost.
 The cast expression's interpretation is ambiguous\index{ambiguous interpretation} if more than one interpretation can be converted at the lowest cost or if the selected interpretation is ambiguous.
 
@@ -1570 +1433 @@
 \lhs{multiplicative-expression}
 \rhs \nonterm{cast-expression}
-\rhs \nonterm{multiplicative-expression} \lstinline$*$ \nonterm{cast-expression}
-\rhs \nonterm{multiplicative-expression} \lstinline$/$ \nonterm{cast-expression}
-\rhs \nonterm{multiplicative-expression} \lstinline$%$ \nonterm{cast-expression}
+\rhs \nonterm{multiplicative-expression} \lstinline@*@ \nonterm{cast-expression}
+\rhs \nonterm{multiplicative-expression} \lstinline@/@ \nonterm{cast-expression}
+\rhs \nonterm{multiplicative-expression} \lstinline@%@ \nonterm{cast-expression}
 \end{syntax}
 
 \rewriterules
 \begin{lstlisting}
-a * b @\rewrite@ ?*?( a, b )@\use{?*?}@
-a / b @\rewrite@ ?/?( a, b )@\use{?/?}@
-a % b @\rewrite@ ?%?( a, b )@\use{?%?}@
+a * b §\rewrite§ ?*?( a, b )§\use{?*?}§
+a / b §\rewrite§ ?/?( a, b )§\use{?/?}§
+a % b §\rewrite§ ?%?( a, b )§\use{?%?}§
 \end{lstlisting}
 
@@ -1606 +1469 @@
         ?*?( _Complex long double, _Complex long double ), ?/?( _Complex long double, _Complex long double );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1624 +1487 @@
 int i;
 long li;
-void eat_double( double );@\use{eat_double}@
+void eat_double( double );§\use{eat_double}§
 eat_double( li % i );
 \end{lstlisting}
-``\lstinline$li % i$'' is rewritten as ``\lstinline$?%?(li, i )$''.
-The valid interpretations of \lstinline$?%?(li, i )$, the cost\index{conversion cost} of converting their arguments, and the cost of converting the result to \lstinline$double$ (assuming no extended integer types are present ) are
+``\lstinline@li % i@'' is rewritten as ``\lstinline@?%?(li, i )@''.
+The valid interpretations of \lstinline@?%?(li, i )@, the cost\index{conversion cost} of converting their arguments, and the cost of converting the result to \lstinline@double@ (assuming no extended integer types are present ) are
 \begin{center}
 \begin{tabular}{lcc} interpretation & argument cost & result cost \\
 \hline 
-\lstinline$ ?%?( (int)li, i )$                                                                          & (unsafe)      & 6     \\
-\lstinline$ ?%?( (unsigned)li,(unsigned)i )$                                            & (unsafe)      & 5     \\
-\lstinline$ ?%?( li, (long)i )$                                                                         & 1                     & 4     \\
-\lstinline$ ?%?( (long unsigned)li,(long unsigned)i )$                          & 3                     & 3     \\
-\lstinline$ ?%?( (long long)li,(long long)i )$                                          & 5                     & 2     \\
-\lstinline$ ?%?( (long long unsigned)li, (long long unsigned)i )$       & 7                     & 1     \\
+\lstinline@ ?%?( (int)li, i )@                                                                          & (unsafe)      & 6     \\
+\lstinline@ ?%?( (unsigned)li,(unsigned)i )@                                            & (unsafe)      & 5     \\
+\lstinline@ ?%?( li, (long)i )@                                                                         & 1                     & 4     \\
+\lstinline@ ?%?( (long unsigned)li,(long unsigned)i )@                          & 3                     & 3     \\
+\lstinline@ ?%?( (long long)li,(long long)i )@                                          & 5                     & 2     \\
+\lstinline@ ?%?( (long long unsigned)li, (long long unsigned)i )@       & 7                     & 1     \\
 \end{tabular}
 \end{center}
-The best interpretation of \lstinline$eat_double( li, i )$ is
-\lstinline$eat_double( (double)?%?(li, (long)i ))$, which has no unsafe conversions and the lowest total cost.
-
-\begin{rationale}
-{\c11} defines most arithmetic operations to apply an \Index{integer promotion} to any argument that belongs to a type that has an \Index{integer conversion rank} less than that of \lstinline$int$.If
-\lstinline$s$ is a \lstinline$short int$, ``\lstinline$s *s$'' does not have type \lstinline$short int$;
-it is treated as ``\lstinline$( (int)s ) * ( (int)s )$'', and has type \lstinline$int$. \CFA matches that pattern;
-it does not predefine ``\lstinline$short ?*?( short, short )$''.
+The best interpretation of \lstinline@eat_double( li, i )@ is
+\lstinline@eat_double( (double)?%?(li, (long)i ))@, which has no unsafe conversions and the lowest total cost.
+
+\begin{rationale}
+{\c11} defines most arithmetic operations to apply an \Index{integer promotion} to any argument that belongs to a type that has an \Index{integer conversion rank} less than that of \lstinline@int@.If
+\lstinline@s@ is a \lstinline@short int@, ``\lstinline@s *s@'' does not have type \lstinline@short int@;
+it is treated as ``\lstinline@( (int)s ) * ( (int)s )@'', and has type \lstinline@int@. \CFA matches that pattern;
+it does not predefine ``\lstinline@short ?*?( short, short )@''.
 
 These ``missing'' operators limit polymorphism.
@@ -1656 +1519 @@
 square( s );
 \end{lstlisting}
-Since \CFA does not define a multiplication operator for \lstinline$short int$,
-\lstinline$square( s )$ is treated as \lstinline$square( (int)s )$, and the result has type
-\lstinline$int$.
+Since \CFA does not define a multiplication operator for \lstinline@short int@,
+\lstinline@square( s )@ is treated as \lstinline@square( (int)s )@, and the result has type
+\lstinline@int@.
 This is mildly surprising, but it follows the {\c11} operator pattern.
 
@@ -1668 +1531 @@
 \end{lstlisting}
 This has no valid interpretations, because \CFA has no conversion from ``array of
-\lstinline$short int$'' to ``array of \lstinline$int$''.
+\lstinline@short int@'' to ``array of \lstinline@int@''.
 The alternatives in such situations include
 \begin{itemize}
 \item
-Defining monomorphic overloadings of \lstinline$product$ for \lstinline$short$ and the other
+Defining monomorphic overloadings of \lstinline@product@ for \lstinline@short@ and the other
 ``small'' types.
 \item
-Defining ``\lstinline$short ?*?( short, short )$'' within the scope containing the call to
-\lstinline$product$.
-\item
-Defining \lstinline$product$ to take as an argument a conversion function from the ``small'' type to the operator's argument type.
+Defining ``\lstinline@short ?*?( short, short )@'' within the scope containing the call to
+\lstinline@product@.
+\item
+Defining \lstinline@product@ to take as an argument a conversion function from the ``small'' type to the operator's argument type.
 \end{itemize}
 \end{rationale}
@@ -1688 +1551 @@
 \lhs{additive-expression}
 \rhs \nonterm{multiplicative-expression}
-\rhs \nonterm{additive-expression} \lstinline$+$ \nonterm{multiplicative-expression}
-\rhs \nonterm{additive-expression} \lstinline$-$ \nonterm{multiplicative-expression}
+\rhs \nonterm{additive-expression} \lstinline@+@ \nonterm{multiplicative-expression}
+\rhs \nonterm{additive-expression} \lstinline@-@ \nonterm{multiplicative-expression}
 \end{syntax}
 
 \rewriterules
 \begin{lstlisting}
-a + b @\rewrite@ ?+?( a, b )@\use{?+?}@
-a - b @\rewrite@ ?-?( a, b )@\use{?-?}@
+a + b §\rewrite§ ?+?( a, b )§\use{?+?}§
+a - b §\rewrite§ ?-?( a, b )§\use{?-?}§
 \end{lstlisting}
 
@@ -1748 +1611 @@
         * ?-?( _Atomic const restrict volatile T *, _Atomic const restrict volatile T * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1758 +1621 @@
 
 \begin{rationale}
-\lstinline$ptrdiff_t$ is an implementation-defined identifier defined in \lstinline$<stddef.h>$ that is synonymous with a signed integral type that is large enough to hold the difference between two pointers.
+\lstinline@ptrdiff_t@ is an implementation-defined identifier defined in \lstinline@<stddef.h>@ that is synonymous with a signed integral type that is large enough to hold the difference between two pointers.
 It seems reasonable to use it for pointer addition as well. (This is technically a difference between \CFA and C, which only specifies that pointer addition uses an \emph{integral} argument.) Hence it is also used for subscripting, which is defined in terms of pointer addition.
-The {\c11} standard uses \lstinline$size_t$ in several cases where a library function takes an argument that is used as a subscript, but \lstinline$size_t$ is unsuitable here because it is an unsigned type.
+The {\c11} standard uses \lstinline@size_t@ in several cases where a library function takes an argument that is used as a subscript, but \lstinline@size_t@ is unsuitable here because it is an unsigned type.
 \end{rationale}
 
@@ -1769 +1632 @@
 \lhs{shift-expression}
 \rhs \nonterm{additive-expression}
-\rhs \nonterm{shift-expression} \lstinline$<<$ \nonterm{additive-expression}
-\rhs \nonterm{shift-expression} \lstinline$>>$ \nonterm{additive-expression}
+\rhs \nonterm{shift-expression} \lstinline@<<@ \nonterm{additive-expression}
+\rhs \nonterm{shift-expression} \lstinline@>>@ \nonterm{additive-expression}
 \end{syntax}
 
 \rewriterules \use{?>>?}%use{?<<?}
 \begin{lstlisting}
-a << b @\rewrite@ ?<<?( a, b )
-a >> b @\rewrite@ ?>>?( a, b )
+a << b §\rewrite§ ?<<?( a, b )
+a >> b §\rewrite§ ?>>?( a, b )
 \end{lstlisting}
 
@@ -1788 +1651 @@
 long long unsigned int ?<<?( long long unsigned int, int ), ?>>?( long long unsigned int, int);
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1808 +1671 @@
 \lhs{relational-expression}
 \rhs \nonterm{shift-expression}
-\rhs \nonterm{relational-expression} \lstinline$< $ \nonterm{shift-expression}
-\rhs \nonterm{relational-expression} \lstinline$> $ \nonterm{shift-expression}
-\rhs \nonterm{relational-expression} \lstinline$<=$ \nonterm{shift-expression}
-\rhs \nonterm{relational-expression} \lstinline$>=$ \nonterm{shift-expression}
+\rhs \nonterm{relational-expression} \lstinline@< @ \nonterm{shift-expression}
+\rhs \nonterm{relational-expression} \lstinline@> @ \nonterm{shift-expression}
+\rhs \nonterm{relational-expression} \lstinline@<=@ \nonterm{shift-expression}
+\rhs \nonterm{relational-expression} \lstinline@>=@ \nonterm{shift-expression}
 \end{syntax}
 
 \rewriterules\use{?>?}\use{?>=?}%use{?<?}%use{?<=?}
 \begin{lstlisting}
-a < b @\rewrite@ ?<?( a, b )
-a > b @\rewrite@ ?>?( a, b )
-a <= b @\rewrite@ ?<=?( a, b )
-a >= b @\rewrite@ ?>=?( a, b )
+a < b §\rewrite§ ?<?( a, b )
+a > b §\rewrite§ ?>?( a, b )
+a <= b §\rewrite§ ?<=?( a, b )
+a >= b §\rewrite§ ?>=?( a, b )
 \end{lstlisting}
 
@@ -1851 +1714 @@
         ?>=?( _Atomic const restrict volatile DT *, _Atomic const restrict volatile DT * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1869 +1732 @@
 \lhs{equality-expression}
 \rhs \nonterm{relational-expression}
-\rhs \nonterm{equality-expression} \lstinline$==$ \nonterm{relational-expression}
-\rhs \nonterm{equality-expression} \lstinline$!=$ \nonterm{relational-expression}
+\rhs \nonterm{equality-expression} \lstinline@==@ \nonterm{relational-expression}
+\rhs \nonterm{equality-expression} \lstinline@!=@ \nonterm{relational-expression}
 \end{syntax}
 
 \rewriterules
 \begin{lstlisting}
-a == b @\rewrite@ ?==?( a, b )@\use{?==?}@
-a != b @\rewrite@ ?!=?( a, b )@\use{?"!=?}@
+a == b §\rewrite§ ?==?( a, b )§\use{?==?}§
+a != b §\rewrite§ ?!=?( a, b )§\use{?"!=?}§
 \end{lstlisting}
 
@@ -1929 +1792 @@
         ?==?( forall( ftype FT2) FT2*, forall( ftype FT3) FT3 * ), ?!=?( forall( ftype FT2) FT2*, forall( ftype FT3) FT3 * );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1937 +1800 @@
 
 \begin{rationale}
-The polymorphic equality operations come in three styles: comparisons between pointers of compatible types, between pointers to \lstinline$void$ and pointers to object types or incomplete types, and between the \Index{null pointer} constant and pointers to any type.
+The polymorphic equality operations come in three styles: comparisons between pointers of compatible types, between pointers to \lstinline@void@ and pointers to object types or incomplete types, and between the \Index{null pointer} constant and pointers to any type.
 In the last case, a special constraint rule for null pointer constant operands has been replaced by a consequence of the \CFA type system.
 \end{rationale}
@@ -1958 +1821 @@
 \lhs{AND-expression}
 \rhs \nonterm{equality-expression}
-\rhs \nonterm{AND-expression} \lstinline$&$ \nonterm{equality-expression}
+\rhs \nonterm{AND-expression} \lstinline@&@ \nonterm{equality-expression}
 \end{syntax}
 
 \rewriterules
 \begin{lstlisting}
-a & b @\rewrite@ ?&?( a, b )@\use{?&?}@
+a & b §\rewrite§ ?&?( a, b )§\use{?&?}§
 \end{lstlisting}
 
@@ -1975 +1838 @@
 long long unsigned int ?&?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -1990 +1853 @@
 \lhs{exclusive-OR-expression}
 \rhs \nonterm{AND-expression}
-\rhs \nonterm{exclusive-OR-expression} \lstinline$^$ \nonterm{AND-expression}
+\rhs \nonterm{exclusive-OR-expression} \lstinline@^@ \nonterm{AND-expression}
 \end{syntax}
 
 \rewriterules
 \begin{lstlisting}
-a ^ b @\rewrite@ ?^?( a, b )@\use{?^?}@
+a ^ b §\rewrite§ ?^?( a, b )§\use{?^?}§
 \end{lstlisting}
 
@@ -2007 +1870 @@
 long long unsigned int ?^?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2022 +1885 @@
 \lhs{inclusive-OR-expression}
 \rhs \nonterm{exclusive-OR-expression}
-\rhs \nonterm{inclusive-OR-expression} \lstinline$|$ \nonterm{exclusive-OR-expression}
+\rhs \nonterm{inclusive-OR-expression} \lstinline@|@ \nonterm{exclusive-OR-expression}
 \end{syntax}
 
 \rewriterules\use{?"|?}
 \begin{lstlisting}
-a | b @\rewrite@ ?|?( a, b )
+a | b §\rewrite§ ?|?( a, b )
 \end{lstlisting}
 
@@ -2039 +1902 @@
 long long unsigned int ?|?( long long unsigned int, long long unsigned int );
 \end{lstlisting}
-For every extended integer type \lstinline$X$ with \Index{integer conversion rank} greater than the rank of \lstinline$int$ there exist
+For every extended integer type \lstinline@X@ with \Index{integer conversion rank} greater than the rank of \lstinline@int@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2054 +1917 @@
 \lhs{logical-AND-expression}
 \rhs \nonterm{inclusive-OR-expression}
-\rhs \nonterm{logical-AND-expression} \lstinline$&&$ \nonterm{inclusive-OR-expression}
+\rhs \nonterm{logical-AND-expression} \lstinline@&&@ \nonterm{inclusive-OR-expression}
 \end{syntax}
 
-\semantics The operands of the expression ``\lstinline$a && b$'' are treated as
-``\lstinline$(int)((a)!=0)$'' and ``\lstinline$(int)((b)!=0)$'', which shall both be unambiguous.
-The expression has only one interpretation, which is of type \lstinline$int$.
-\begin{rationale}
-When the operands of a logical expression are values of built-in types, and ``\lstinline$!=$'' has not been redefined for those types, the compiler can optimize away the function calls.
-
-A common C idiom omits comparisons to \lstinline$0$ in the controlling expressions of loops and
-\lstinline$if$ statements.
-For instance, the loop below iterates as long as \lstinline$rp$ points at a \lstinline$Rational$ value that is non-zero.
-
-\begin{lstlisting}
-extern otype Rational;@\use{Rational}@
-extern const Rational 0;@\use{0}@
+\semantics The operands of the expression ``\lstinline@a && b@'' are treated as
+``\lstinline@(int)((a)!=0)@'' and ``\lstinline@(int)((b)!=0)@'', which shall both be unambiguous.
+The expression has only one interpretation, which is of type \lstinline@int@.
+\begin{rationale}
+When the operands of a logical expression are values of built-in types, and ``\lstinline@!=@'' has not been redefined for those types, the compiler can optimize away the function calls.
+
+A common C idiom omits comparisons to \lstinline@0@ in the controlling expressions of loops and
+\lstinline@if@ statements.
+For instance, the loop below iterates as long as \lstinline@rp@ points at a \lstinline@Rational@ value that is non-zero.
+
+\begin{lstlisting}
+extern otype Rational;§\use{Rational}§
+extern const Rational 0;§\use{0}§
 extern int ?!=?( Rational, Rational );
 Rational *rp;
 while ( rp && *rp ) { ... }
 \end{lstlisting}
-The logical expression calls the \lstinline$Rational$ inequality operator, passing it \lstinline$*rp$ and the \lstinline$Rational 0$, and getting a 1 or 0 as a result.
-In contrast, {\CC} would apply a programmer-defined \lstinline$Rational$-to-\lstinline$int$ conversion to \lstinline$*rp$ in the equivalent situation.
-The conversion to \lstinline$int$ would produce a general integer value, which is unfortunate, and possibly dangerous if the conversion was not written with this situation in mind.
+The logical expression calls the \lstinline@Rational@ inequality operator, passing it \lstinline@*rp@ and the \lstinline@Rational 0@, and getting a 1 or 0 as a result.
+In contrast, {\CC} would apply a programmer-defined \lstinline@Rational@-to-\lstinline@int@ conversion to \lstinline@*rp@ in the equivalent situation.
+The conversion to \lstinline@int@ would produce a general integer value, which is unfortunate, and possibly dangerous if the conversion was not written with this situation in mind.
 \end{rationale}
 
@@ -2085 +1948 @@
 \lhs{logical-OR-expression}
 \rhs \nonterm{logical-AND-expression}
-\rhs \nonterm{logical-OR-expression} \lstinline$||$ \nonterm{logical-AND-expression}
+\rhs \nonterm{logical-OR-expression} \lstinline@||@ \nonterm{logical-AND-expression}
 \end{syntax}
 
 \semantics
 
-The operands of the expression ``\lstinline$a || b$'' are treated as ``\lstinline$(int)((a)!=0)$'' and ``\lstinline$(int)((b))!=0)$'', which shall both be unambiguous.
-The expression has only one interpretation, which is of type \lstinline$int$.
+The operands of the expression ``\lstinline@a || b@'' are treated as ``\lstinline@(int)((a)!=0)@'' and ``\lstinline@(int)((b))!=0)@'', which shall both be unambiguous.
+The expression has only one interpretation, which is of type \lstinline@int@.
 
 
@@ -2099 +1962 @@
 \lhs{conditional-expression}
 \rhs \nonterm{logical-OR-expression}
-\rhs \nonterm{logical-OR-expression} \lstinline$?$ \nonterm{expression}
-         \lstinline$:$ \nonterm{conditional-expression}
+\rhs \nonterm{logical-OR-expression} \lstinline@?@ \nonterm{expression}
+         \lstinline@:@ \nonterm{conditional-expression}
 \end{syntax}
 
 \semantics
-In the conditional expression\use{?:} ``\lstinline$a?b:c$'', if the second and third operands both have an interpretation with \lstinline$void$ type, then the expression has an interpretation with type \lstinline$void$, equivalent to
+In the conditional expression\use{?:} ``\lstinline@a?b:c@'', if the second and third operands both have an interpretation with \lstinline@void@ type, then the expression has an interpretation with type \lstinline@void@, equivalent to
 \begin{lstlisting}
 ( int)(( a)!=0) ? ( void)( b) : ( void)( c)
 \end{lstlisting}
 
-If the second and third operands both have interpretations with non-\lstinline$void$ types, the expression is treated as if it were the call ``\lstinline$cond((a)!=0, b, c)$'', with \lstinline$cond$ declared as
+If the second and third operands both have interpretations with non-\lstinline@void@ types, the expression is treated as if it were the call ``\lstinline@cond((a)!=0, b, c)@'', with \lstinline@cond@ declared as
 \begin{lstlisting}
 forall( otype T ) T cond( int, T, T );
@@ -2161 +2024 @@
 rand() ? i : l;
 \end{lstlisting}
-The best interpretation infers the expression's type to be \lstinline$long$ and applies the safe
-\lstinline$int$-to-\lstinline$long$ conversion to \lstinline$i$.
+The best interpretation infers the expression's type to be \lstinline@long@ and applies the safe
+\lstinline@int@-to-\lstinline@long@ conversion to \lstinline@i@.
 
 \begin{lstlisting}
@@ -2169 +2032 @@
 rand() ? cip : vip;
 \end{lstlisting}
-The expression has type \lstinline$const volatile int *$, with safe conversions applied to the second and third operands to add \lstinline$volatile$ and \lstinline$const$ qualifiers, respectively.
+The expression has type \lstinline@const volatile int *@, with safe conversions applied to the second and third operands to add \lstinline@volatile@ and \lstinline@const@ qualifiers, respectively.
 
 \begin{lstlisting}
 rand() ? cip : 0;
 \end{lstlisting}
-The expression has type \lstinline$const int *$, with a specialization conversion applied to
-\lstinline$0$.
+The expression has type \lstinline@const int *@, with a specialization conversion applied to
+\lstinline@0@.
 
 
@@ -2186 +2049 @@
          \nonterm{assignment-expression}
 \lhs{assignment-operator} one of
-\rhs \lstinline$=$\ \ \lstinline$*=$\ \ \lstinline$/=$\ \ \lstinline$%=$\ \ \lstinline$+=$\ \ \lstinline$-=$\ \  
-         \lstinline$<<=$\ \ \lstinline$>>=$\ \ \lstinline$&=$\ \ \lstinline$^=$\ \ \lstinline$|=$
+\rhs \lstinline@=@\ \ \lstinline@*=@\ \ \lstinline@/=@\ \ \lstinline@%=@\ \ \lstinline@+=@\ \ \lstinline@-=@\ \  
+         \lstinline@<<=@\ \ \lstinline@>>=@\ \ \lstinline@&=@\ \ \lstinline@^=@\ \ \lstinline@|=@
 \end{syntax}
 
@@ -2196 +2059 @@
 \use{?>>=?}\use{?&=?}\use{?^=?}\use{?"|=?}%use{?<<=?}
 \begin{lstlisting}
-a @$\leftarrow$@ b @\rewrite@ ?@$\leftarrow$@?( &( a ), b )
+a §$\leftarrow$§ b §\rewrite§ ?§$\leftarrow$§?( &( a ), b )
 \end{lstlisting}
 
 \semantics
 Each interpretation of the left operand of an assignment expression is considered separately.
-For each interpretation that is a bit-field or is declared with the \lstinline$register$ storage class specifier, the expression has one valid interpretation, with the type of the left operand.
+For each interpretation that is a bit-field or is declared with the \lstinline@register@ storage class specifier, the expression has one valid interpretation, with the type of the left operand.
 The right operand is cast to that type, and the assignment expression is ambiguous if either operand is.
 For the remaining interpretations, the expression is rewritten, and the interpretations of the assignment expression are the interpretations of the corresponding function call.
@@ -2434 +2297 @@
 \end{lstlisting}
 \begin{rationale}
-The pattern of overloadings for simple assignment resembles that of pointer increment and decrement, except that the polymorphic pointer assignment functions declare a \lstinline$dtype$ parameter, instead of a \lstinline$type$ parameter, because the left operand may be a pointer to an incomplete type.
-\end{rationale}
-
-For every complete structure or union type \lstinline$S$ there exist
+The pattern of overloadings for simple assignment resembles that of pointer increment and decrement, except that the polymorphic pointer assignment functions declare a \lstinline@dtype@ parameter, instead of a \lstinline@type@ parameter, because the left operand may be a pointer to an incomplete type.
+\end{rationale}
+
+For every complete structure or union type \lstinline@S@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2443 +2306 @@
 \end{lstlisting}
 
-For every extended integer type \lstinline$X$ there exist
+For every extended integer type \lstinline@X@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2449 +2312 @@
 \end{lstlisting}
 
-For every complete enumerated type \lstinline$E$ there exist
+For every complete enumerated type \lstinline@E@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2455 +2318 @@
 \end{lstlisting}
 \begin{rationale}
-The right-hand argument is \lstinline$int$ because enumeration constants have type \lstinline$int$.
+The right-hand argument is \lstinline@int@ because enumeration constants have type \lstinline@int@.
 \end{rationale}
 
@@ -2716 +2579 @@
 \end{lstlisting}
 
-For every extended integer type \lstinline$X$ there exist
+For every extended integer type \lstinline@X@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2731 +2594 @@
 \end{lstlisting}
 
-For every complete enumerated type \lstinline$E$ there exist
+For every complete enumerated type \lstinline@E@ there exist
 % Don't use predefined: keep this out of prelude.cf.
 \begin{lstlisting}
@@ -2752 +2615 @@
 \lhs{expression}
 \rhs \nonterm{assignment-expression}
-\rhs \nonterm{expression} \lstinline$,$ \nonterm{assignment-expression}
+\rhs \nonterm{expression} \lstinline@,@ \nonterm{assignment-expression}
 \end{syntax}
 
 \semantics
-In the comma expression ``\lstinline$a, b$'', the first operand is interpreted as
-``\lstinline$( void )(a)$'', which shall be unambiguous\index{ambiguous interpretation}.
+In the comma expression ``\lstinline@a, b@'', the first operand is interpreted as
+``\lstinline@( void )(a)@'', which shall be unambiguous\index{ambiguous interpretation}.
 The interpretations of the expression are the interpretations of the second operand.
 
@@ -2792 +2655 @@
 { ... }
 \end{lstlisting}
-Without the rule, \lstinline$Complex$ would be a type in the first case, and a parameter name in the second.
+Without the rule, \lstinline@Complex@ would be a type in the first case, and a parameter name in the second.
 \end{rationale}
 
@@ -2818 +2681 @@
 \examples
 \begin{lstlisting}
-struct point {@\impl{point}@
+struct point {§\impl{point}§
         int x, y;
 };
-struct color_point {@\impl{color_point}@
+struct color_point {§\impl{color_point}§
         enum { RED, BLUE, GREEN } color;
         struct point;
@@ -2828 +2691 @@
 cp.x = 0;
 cp.color = RED;
-struct literal {@\impl{literal}@
+struct literal {§\impl{literal}§
         enum { NUMBER, STRING } tag;
         union {
@@ -2849 +2712 @@
 \begin{syntax}
 \lhs{forall-specifier}
-\rhs \lstinline$forall$ \lstinline$($ \nonterm{type-parameter-list} \lstinline$)$
+\rhs \lstinline@forall@ \lstinline@(@ \nonterm{type-parameter-list} \lstinline@)@
 \end{syntax}
 
@@ -2861 +2724 @@
 } mkPair( T, T ); // illegal 
 \end{lstlisting}
-If an instance of \lstinline$struct Pair$ was declared later in the current scope, what would the members' type be?
+If an instance of \lstinline@struct Pair@ was declared later in the current scope, what would the members' type be?
 \end{rationale}
 \end{comment}
@@ -2868 +2731 @@
 The \nonterm{type-parameter-list}s and assertions of the \nonterm{forall-specifier}s declare type identifiers, function and object identifiers with \Index{no linkage}.
 
-If, in the declaration ``\lstinline$T D$'', \lstinline$T$ contains \nonterm{forall-specifier}s and
-\lstinline$D$ has the form
-\begin{lstlisting}
-D( @\normalsize\nonterm{parameter-type-list}@ )
-\end{lstlisting} then a type identifier declared by one of the \nonterm{forall-specifier}s is an \define{inferred parameter} of the function declarator if and only if it is not an inferred parameter of a function declarator in \lstinline$D$, and it is used in the type of a parameter in the following
+If, in the declaration ``\lstinline@T D@'', \lstinline@T@ contains \nonterm{forall-specifier}s and
+\lstinline@D@ has the form
+\begin{lstlisting}
+D( §\normalsize\nonterm{parameter-type-list}§ )
+\end{lstlisting} then a type identifier declared by one of the \nonterm{forall-specifier}s is an \define{inferred parameter} of the function declarator if and only if it is not an inferred parameter of a function declarator in \lstinline@D@, and it is used in the type of a parameter in the following
 \nonterm{type-parameter-list} or it and an inferred parameter are used as arguments of a
 \Index{specification} in one of the \nonterm{forall-specifier}s.
@@ -2883 +2746 @@
 If this restriction were lifted, it would be possible to write
 \begin{lstlisting}
-forall( otype T ) T * alloc( void );@\use{alloc}@ int *p = alloc();
-\end{lstlisting}
-Here \lstinline$alloc()$ would receive \lstinline$int$ as an inferred argument, and return an
-\lstinline$int *$.
-In general, if a call to \lstinline$alloc()$ is a subexpression of an expression involving polymorphic functions and overloaded identifiers, there could be considerable distance between the call and the subexpression that causes \lstinline$T$ to be bound.
-
-With the current restriction, \lstinline$alloc()$ must be given an argument that determines
-\lstinline$T$:
-\begin{lstlisting}
-forall( otype T ) T * alloc( T initial_value );@\use{alloc}@
+forall( otype T ) T * alloc( void );§\use{alloc}§ int *p = alloc();
+\end{lstlisting}
+Here \lstinline@alloc()@ would receive \lstinline@int@ as an inferred argument, and return an
+\lstinline@int *@.
+In general, if a call to \lstinline@alloc()@ is a subexpression of an expression involving polymorphic functions and overloaded identifiers, there could be considerable distance between the call and the subexpression that causes \lstinline@T@ to be bound.
+
+With the current restriction, \lstinline@alloc()@ must be given an argument that determines
+\lstinline@T@:
+\begin{lstlisting}
+forall( otype T ) T * alloc( T initial_value );§\use{alloc}§
 \end{lstlisting}
 \end{rationale}
@@ -2917 +2780 @@
 forall( otype T ) T fT( T );
 \end{lstlisting}
-\lstinline$fi()$ takes an \lstinline$int$ and returns an \lstinline$int$. \lstinline$fT()$ takes a
-\lstinline$T$ and returns a \lstinline$T$, for any type \lstinline$T$.
+\lstinline@fi()@ takes an \lstinline@int@ and returns an \lstinline@int@. \lstinline@fT()@ takes a
+\lstinline@T@ and returns a \lstinline@T@, for any type \lstinline@T@.
 \begin{lstlisting}
 int (*pfi )( int ) = fi;
 forall( otype T ) T (*pfT )( T ) = fT;
 \end{lstlisting}
-\lstinline$pfi$ and \lstinline$pfT$ are pointers to functions. \lstinline$pfT$ is not polymorphic, but the function it points at is.
+\lstinline@pfi@ and \lstinline@pfT@ are pointers to functions. \lstinline@pfT@ is not polymorphic, but the function it points at is.
 \begin{lstlisting}
 int (*fvpfi( void ))( int ) {
@@ -2932 +2795 @@
 }
 \end{lstlisting}
-\lstinline$fvpfi()$ and \lstinline$fvpfT()$ are functions taking no arguments and returning pointers to functions. \lstinline$fvpfT()$ is monomorphic, but the function that its return value points at is polymorphic.
+\lstinline@fvpfi()@ and \lstinline@fvpfT()@ are functions taking no arguments and returning pointers to functions. \lstinline@fvpfT()@ is monomorphic, but the function that its return value points at is polymorphic.
 \begin{lstlisting}
 forall( otype T ) int ( *fTpfi( T ) )( int );
@@ -2938 +2801 @@
 forall( otype T, otype U ) U ( *fTpfU( T ) )( U );
 \end{lstlisting}
-\lstinline$fTpfi()$ is a polymorphic function that returns a pointer to a monomorphic function taking an integer and returning an integer.
-It could return \lstinline$pfi$. \lstinline$fTpfT()$ is subtle: it is a polymorphic function returning a \emph{monomorphic} function taking and returning
-\lstinline$T$, where \lstinline$T$ is an inferred parameter of \lstinline$fTpfT()$.
-For instance, in the expression ``\lstinline$fTpfT(17)$'', \lstinline$T$ is inferred to be \lstinline$int$, and the returned value would have type \lstinline$int ( * )( int )$. ``\lstinline$fTpfT(17)(13)$'' and
-``\lstinline$fTpfT("yes")("no")$'' are legal, but ``\lstinline$fTpfT(17)("no")$'' is illegal.
-\lstinline$fTpfU()$ is polymorphic ( in type \lstinline$T$), and returns a pointer to a function that is polymorphic ( in type \lstinline$U$). ``\lstinline$f5(17)("no")$'' is a legal expression of type
-\lstinline$char *$.
+\lstinline@fTpfi()@ is a polymorphic function that returns a pointer to a monomorphic function taking an integer and returning an integer.
+It could return \lstinline@pfi@. \lstinline@fTpfT()@ is subtle: it is a polymorphic function returning a \emph{monomorphic} function taking and returning
+\lstinline@T@, where \lstinline@T@ is an inferred parameter of \lstinline@fTpfT()@.
+For instance, in the expression ``\lstinline@fTpfT(17)@'', \lstinline@T@ is inferred to be \lstinline@int@, and the returned value would have type \lstinline@int ( * )( int )@. ``\lstinline@fTpfT(17)(13)@'' and
+``\lstinline@fTpfT("yes")("no")@'' are legal, but ``\lstinline@fTpfT(17)("no")@'' is illegal.
+\lstinline@fTpfU()@ is polymorphic ( in type \lstinline@T@), and returns a pointer to a function that is polymorphic ( in type \lstinline@U@). ``\lstinline@f5(17)("no")@'' is a legal expression of type
+\lstinline@char *@.
 \begin{lstlisting}
 forall( otype T, otype U, otype V ) U * f( T *, U, V * const );
 forall( otype U, otype V, otype W ) U * g( V *, U, W * const );
 \end{lstlisting}
-The functions \lstinline$f()$ and \lstinline$g()$ have compatible types.
+The functions \lstinline@f()@ and \lstinline@g()@ have compatible types.
 Let \(f\) and \(g\) be their types;
-then \(f_1\) = \lstinline$T$, \(f_2\) = \lstinline$U$, \(f_3\) = \lstinline$V$, \(g_1\)
-= \lstinline$V$, \(g_2\) = \lstinline$U$, and \(g_3\) = \lstinline$W$.
+then \(f_1\) = \lstinline@T@, \(f_2\) = \lstinline@U@, \(f_3\) = \lstinline@V@, \(g_1\)
+= \lstinline@V@, \(g_2\) = \lstinline@U@, and \(g_3\) = \lstinline@W@.
 Replacing every \(f_i\) by \(g_i\) in \(f\) gives
 \begin{lstlisting}
@@ -2958 +2821 @@
 \end{lstlisting} which has a return type and parameter list that is compatible with \(g\).
 \begin{rationale}
-The word ``\lstinline$type$'' in a forall specifier is redundant at the moment, but I want to leave room for inferred parameters of ordinary types in case parameterized types get added one day.
+The word ``\lstinline@type@'' in a forall specifier is redundant at the moment, but I want to leave room for inferred parameters of ordinary types in case parameterized types get added one day.
 
 Even without parameterized types, I might try to allow
@@ -2984 +2847 @@
 \subsection{Type qualifiers}
 
-\CFA defines a new type qualifier \lstinline$lvalue$\impl{lvalue}\index{lvalue}.
+\CFA defines a new type qualifier \lstinline@lvalue@\impl{lvalue}\index{lvalue}.
 \begin{syntax}
 \oldlhs{type-qualifier}
-\rhs \lstinline$lvalue$
+\rhs \lstinline@lvalue@
 \end{syntax}
 
 \constraints
-\lstinline$restrict$\index{register@{\lstinline$restrict$}} Types other than type parameters and pointer types whose referenced type is an object type shall not be restrict-qualified.
+\Indexc{restrict} Types other than type parameters and pointer types whose referenced type is an object type shall not be restrict-qualified.
 
 \semantics
-An object's type may be a restrict-qualified type parameter. \lstinline$restrict$ does not establish any special semantics in that case.
+An object's type may be a restrict-qualified type parameter.
+\lstinline@restrict@ does not establish any special semantics in that case.
 
 \begin{rationale}
@@ -3000 +2864 @@
 \end{rationale}
 
-\lstinline$lvalue$ may be used to qualify the return type of a function type.
-Let \lstinline$T$ be an unqualified version of a type;
+\lstinline@lvalue@ may be used to qualify the return type of a function type.
+Let \lstinline@T@ be an unqualified version of a type;
 then the result of calling a function with return type
-\lstinline$lvalue T$ is a \Index{modifiable lvalue} of type \lstinline$T$.
-\lstinline$const$\use{const} and \lstinline$volatile$\use{volatile} qualifiers may also be added to indicate that the function result is a constant or volatile lvalue.
-\begin{rationale}
-The \lstinline$const$ and \lstinline$volatile$ qualifiers can only be sensibly used to qualify the return type of a function if the \lstinline$lvalue$ qualifier is also used.
+\lstinline@lvalue T@ is a \Index{modifiable lvalue} of type \lstinline@T@.
+\lstinline@const@\use{const} and \lstinline@volatile@\use{volatile} qualifiers may also be added to indicate that the function result is a constant or volatile lvalue.
+\begin{rationale}
+The \lstinline@const@ and \lstinline@volatile@ qualifiers can only be sensibly used to qualify the return type of a function if the \lstinline@lvalue@ qualifier is also used.
 \end{rationale}
 
@@ -3013 +2877 @@
 
 \begin{rationale}
-\lstinline$lvalue$ provides some of the functionality of {\CC}'s ``\lstinline$T&$'' ( reference to object of type \lstinline$T$) type.
+\lstinline@lvalue@ provides some of the functionality of {\CC}'s ``\lstinline@T&@'' ( reference to object of type \lstinline@T@) type.
 Reference types have four uses in {\CC}.
 \begin{itemize}
 \item
-They are necessary for user-defined operators that return lvalues, such as ``subscript'' and
-``dereference''.
-
-\item
-A reference can be used to define an alias for a complicated lvalue expression, as a way of getting some of the functionality of the Pascal \lstinline$with$ statement.
+They are necessary for user-defined operators that return lvalues, such as ``subscript'' and ``dereference''.
+
+\item
+A reference can be used to define an alias for a complicated lvalue expression, as a way of getting some of the functionality of the Pascal \lstinline@with@ statement.
 The following {\CC} code gives an example.
 \begin{lstlisting}
@@ -3034 +2897 @@
 A reference parameter can be used to allow a function to modify an argument without forcing the caller to pass the address of the argument.
 This is most useful for user-defined assignment operators.
-In {\CC}, plain assignment is done by a function called ``\lstinline$operator=$'', and the two expressions
+In {\CC}, plain assignment is done by a function called ``\lstinline@operator=@'', and the two expressions
 \begin{lstlisting}
 a = b;
 operator=( a, b );
 \end{lstlisting} are equivalent.
-If \lstinline$a$ and \lstinline$b$ are of type \lstinline$T$, then the first parameter of \lstinline$operator=$ must have type ``\lstinline$T&$''.
+If \lstinline@a@ and \lstinline@b@ are of type \lstinline@T@, then the first parameter of \lstinline@operator=@ must have type ``\lstinline@T&@''.
 It cannot have type
-\lstinline$T$, because then assignment couldn't alter the variable, and it can't have type
-``\lstinline$T *$'', because the assignment would have to be written ``\lstinline$&a = b;$''.
-
-In the case of user-defined operators, this could just as well be handled by using pointer types and by changing the rewrite rules so that ``\lstinline$a = b;$'' is equivalent to
-``\lstinline$operator=(&( a), b )$''.
-Reference parameters of ``normal'' functions are Bad Things, because they remove a useful property of C function calls: an argument can only be modified by a function if it is preceded by ``\lstinline$&$''.
+\lstinline@T@, because then assignment couldn't alter the variable, and it can't have type
+``\lstinline@T *@'', because the assignment would have to be written ``\lstinline@&a = b;@''.
+
+In the case of user-defined operators, this could just as well be handled by using pointer types and by changing the rewrite rules so that ``\lstinline@a = b;@'' is equivalent to
+``\lstinline@operator=(&( a), b )@''.
+Reference parameters of ``normal'' functions are Bad Things, because they remove a useful property of C function calls: an argument can only be modified by a function if it is preceded by ``\lstinline@&@''.
 
 \item
 References to \Index{const-qualified} types can be used instead of value parameters.  Given the
-{\CC} function call ``\lstinline$fiddle( a_thing )$'', where the type of \lstinline$a_thing$ is
-\lstinline$Thing$, the type of \lstinline$fiddle$ could be either of
+{\CC} function call ``\lstinline@fiddle( a_thing )@'', where the type of \lstinline@a_thing@ is
+\lstinline@Thing@, the type of \lstinline@fiddle@ could be either of
 \begin{lstlisting}
 void fiddle( Thing );
 void fiddle( const Thing & );
 \end{lstlisting}
-If the second form is used, then constructors and destructors are not invoked to create a temporary variable at the call site ( and it is bad style for the caller to make any assumptions about such things), and within \lstinline$fiddle$ the parameter is subject to the usual problems caused by aliases.
-The reference form might be chosen for efficiency's sake if \lstinline$Thing$s are too large or their constructors or destructors are too expensive.
+If the second form is used, then constructors and destructors are not invoked to create a temporary variable at the call site ( and it is bad style for the caller to make any assumptions about such things), and within \lstinline@fiddle@ the parameter is subject to the usual problems caused by aliases.
+The reference form might be chosen for efficiency's sake if \lstinline@Thing@s are too large or their constructors or destructors are too expensive.
 An implementation may switch between them without causing trouble for well-behaved clients.
 This leaves the implementor to define ``too large'' and ``too expensive''.
@@ -3065 +2928 @@
 void fiddle( const volatile Thing );
 \end{lstlisting} with call-by-reference.
-Since it knows all about the size of \lstinline$Thing$s and the parameter passing mechanism, it should be able to come up with a better definition of ``too large'', and may be able to make a good guess at ``too expensive''.
+Since it knows all about the size of \lstinline@Thing@s and the parameter passing mechanism, it should be able to come up with a better definition of ``too large'', and may be able to make a good guess at ``too expensive''.
 \end{itemize}
 
@@ -3085 +2948 @@
 \begin{syntax}
 \lhs{spec-definition}
-\rhs \lstinline$spec$ \nonterm{identifier} 
-        \lstinline$($ \nonterm{type-parameter-list} \lstinline$)$
-        \lstinline${$ \nonterm{spec-declaration-list}\opt \lstinline$}$
+\rhs \lstinline@spec@ \nonterm{identifier} 
+        \lstinline@(@ \nonterm{type-parameter-list} \lstinline@)@
+        \lstinline@{@ \nonterm{spec-declaration-list}\opt \lstinline@}@
 \lhs{spec-declaration-list}
-\rhs \nonterm{spec-declaration} \lstinline$;$
-\rhs \nonterm{spec-declaration-list} \nonterm{spec-declaration} \lstinline$;$
+\rhs \nonterm{spec-declaration} \lstinline@;@
+\rhs \nonterm{spec-declaration-list} \nonterm{spec-declaration} \lstinline@;@
 \lhs{spec-declaration}
 \rhs \nonterm{specifier-qualifier-list} \nonterm{declarator-list}
 \lhs{declarator-list}
 \rhs \nonterm{declarator}
-\rhs \nonterm{declarator-list} \lstinline$,$ \nonterm{declarator}
+\rhs \nonterm{declarator-list} \lstinline@,@ \nonterm{declarator}
 \end{syntax}
 \begin{rationale}
@@ -3117 +2980 @@
 \rhs \nonterm{assertion-list} \nonterm{assertion}
 \lhs{assertion}
-\rhs \lstinline$|$ \nonterm{identifier} \lstinline$($ \nonterm{type-name-list} \lstinline$)$
-\rhs \lstinline$|$ \nonterm{spec-declaration}
+\rhs \lstinline@|@ \nonterm{identifier} \lstinline@(@ \nonterm{type-name-list} \lstinline@)@
+\rhs \lstinline@|@ \nonterm{spec-declaration}
 \lhs{type-name-list}
 \rhs \nonterm{type-name}
-\rhs \nonterm{type-name-list} \lstinline$,$ \nonterm{type-name}
+\rhs \nonterm{type-name-list} \lstinline@,@ \nonterm{type-name}
 \end{syntax}
 
@@ -3128 +2991 @@
 The \nonterm{type-name-list} shall contain one \nonterm{type-name} argument for each \nonterm{type-parameter} in that specification's \nonterm{spec-parameter-list}.
 If the
-\nonterm{type-parameter} uses type-class \lstinline$type$\use{type}, the argument shall be the type name of an \Index{object type};
-if it uses \lstinline$dtype$, the argument shall be the type name of an object type or an \Index{incomplete type};
-and if it uses \lstinline$ftype$, the argument shall be the type name of a \Index{function type}.
+\nonterm{type-parameter} uses type-class \lstinline@type@\use{type}, the argument shall be the type name of an \Index{object type};
+if it uses \lstinline@dtype@, the argument shall be the type name of an object type or an \Index{incomplete type};
+and if it uses \lstinline@ftype@, the argument shall be the type name of a \Index{function type}.
 
 \semantics
@@ -3143 +3006 @@
 \examples
 \begin{lstlisting}
-forall( otype T | T ?*?( T, T ))@\use{?*?}@
-T square( T val ) {@\impl{square}@
+forall( otype T | T ?*?( T, T ))§\use{?*?}§
+T square( T val ) {§\impl{square}§
         return val + val;
 }
-trait summable( otype T ) {@\impl{summable}@
-        T ?+=?( T *, T );@\use{?+=?}@
-        const T 0;@\use{0}@
+trait summable( otype T ) {§\impl{summable}§
+        T ?+=?( T *, T );§\use{?+=?}§
+        const T 0;§\use{0}§
 };
-trait list_of( otype List, otype Element ) {@\impl{list_of}@
+trait list_of( otype List, otype Element ) {§\impl{list_of}§
         Element car( List );
         List cdr( List );
@@ -3160 +3023 @@
 trait sum_list( otype List, otype Element | summable( Element ) | list_of( List, Element ) ) {};
 \end{lstlisting}
-\lstinline$sum_list$ contains seven declarations, which describe a list whose elements can be added up.
-The assertion ``\lstinline$|sum_list( i_list, int )$''\use{sum_list} produces the assertion parameters
+\lstinline@sum_list@ contains seven declarations, which describe a list whose elements can be added up.
+The assertion ``\lstinline@|sum_list( i_list, int )@''\use{sum_list} produces the assertion parameters
 \begin{lstlisting}
 int ?+=?( int *, int );
@@ -3178 +3041 @@
 \lhs{type-parameter-list}
 \rhs \nonterm{type-parameter}
-\rhs \nonterm{type-parameter-list} \lstinline$,$ \nonterm{type-parameter}
+\rhs \nonterm{type-parameter-list} \lstinline@,@ \nonterm{type-parameter}
 \lhs{type-parameter}
 \rhs \nonterm{type-class} \nonterm{identifier} \nonterm{assertion-list}\opt
 \lhs{type-class}
-\rhs \lstinline$type$
-\rhs \lstinline$dtype$
-\rhs \lstinline$ftype$
+\rhs \lstinline@type@
+\rhs \lstinline@dtype@
+\rhs \lstinline@ftype@
 \lhs{type-declaration}
-\rhs \nonterm{storage-class-specifier}\opt \lstinline$type$ \nonterm{type-declarator-list} \verb|;|
+\rhs \nonterm{storage-class-specifier}\opt \lstinline@type@ \nonterm{type-declarator-list} \verb|;|
 \lhs{type-declarator-list}
 \rhs \nonterm{type-declarator}
-\rhs \nonterm{type-declarator-list} \lstinline$,$ \nonterm{type-declarator}
+\rhs \nonterm{type-declarator-list} \lstinline@,@ \nonterm{type-declarator}
 \lhs{type-declarator}
-\rhs \nonterm{identifier} \nonterm{assertion-list}\opt \lstinline$=$ \nonterm{type-name}
+\rhs \nonterm{identifier} \nonterm{assertion-list}\opt \lstinline@=@ \nonterm{type-name}
 \rhs \nonterm{identifier} \nonterm{assertion-list}\opt
 \end{syntax}
@@ -3202 +3065 @@
 
 An identifier declared by a \nonterm{type-parameter} has \Index{no linkage}.
-Identifiers declared with type-class \lstinline$type$\use{type} are \Index{object type}s;
+Identifiers declared with type-class \lstinline@type@\use{type} are \Index{object type}s;
 those declared with type-class
-\lstinline$dtype$\use{dtype} are \Index{incomplete type}s;
+\lstinline@dtype@\use{dtype} are \Index{incomplete type}s;
 and those declared with type-class
-\lstinline$ftype$\use{ftype} are \Index{function type}s.
+\lstinline@ftype@\use{ftype} are \Index{function type}s.
 The identifier has \Index{block scope} that terminates at the end of the \nonterm{spec-declaration-list} or polymorphic function that contains the \nonterm{type-parameter}.
 
@@ -3214 +3077 @@
 Within the scope of the declaration, \Index{implicit conversion}s can be performed between the defined type and the implementation type, and between pointers to the defined type and pointers to the implementation type.
 
-A type declaration without an \Index{initializer} and without a \Index{storage-class specifier} or with storage-class specifier \lstinline$static$\use{static} defines an \Index{incomplete type}.
+A type declaration without an \Index{initializer} and without a \Index{storage-class specifier} or with storage-class specifier \lstinline@static@\use{static} defines an \Index{incomplete type}.
 If a
 \Index{translation unit} or \Index{block} contains one or more such declarations for an identifier, it must contain exactly one definition of the identifier ( but not in an enclosed block, which would define a new type known only within that block).
@@ -3234 +3097 @@
 
 A type declaration without an initializer and with \Index{storage-class specifier}
-\lstinline$extern$\use{extern} is an \define{opaque type declaration}.
+\lstinline@extern@\use{extern} is an \define{opaque type declaration}.
 Opaque types are
 \Index{object type}s.
@@ -3249 +3112 @@
 \end{rationale}
 
-An \Index{incomplete type} which is not a qualified version\index{qualified type} of a type is a value of \Index{type-class} \lstinline$dtype$.
-An object type\index{object types} which is not a qualified version of a type is a value of type-classes \lstinline$type$ and \lstinline$dtype$.
+An \Index{incomplete type} which is not a qualified version\index{qualified type} of a type is a value of \Index{type-class} \lstinline@dtype@.
+An object type\index{object types} which is not a qualified version of a type is a value of type-classes \lstinline@type@ and \lstinline@dtype@.
 A
-\Index{function type} is a value of type-class \lstinline$ftype$.
+\Index{function type} is a value of type-class \lstinline@ftype@.
 \begin{rationale}
 Syntactically, a type value is a \nonterm{type-name}, which is a declaration for an object which omits the identifier being declared.
@@ -3262 +3125 @@
 Type qualifiers are a weak point of C's type system.
 Consider the standard library function
-\lstinline$strchr()$ which, given a string and a character, returns a pointer to the first occurrence of the character in the string.
-\begin{lstlisting}
-char *strchr( const char *s, int c ) {@\impl{strchr}@
+\lstinline@strchr()@ which, given a string and a character, returns a pointer to the first occurrence of the character in the string.
+\begin{lstlisting}
+char *strchr( const char *s, int c ) {§\impl{strchr}§
         char real_c = c; // done because c was declared as int. 
         for ( ; *s != real_c; s++ )
@@ -3271 +3134 @@
 }
 \end{lstlisting}
-The parameter \lstinline$s$ must be \lstinline$const char *$, because \lstinline$strchr()$ might be used to search a constant string, but the return type must be \lstinline$char *$, because the result might be used to modify a non-constant string.
+The parameter \lstinline@s@ must be \lstinline@const char *@, because \lstinline@strchr()@ might be used to search a constant string, but the return type must be \lstinline@char *@, because the result might be used to modify a non-constant string.
 Hence the body must perform a cast, and ( even worse)
-\lstinline$strchr()$ provides a type-safe way to attempt to modify constant strings.
-What is needed is some way to say that \lstinline$s$'s type might contain qualifiers, and the result type has exactly the same qualifiers.
+\lstinline@strchr()@ provides a type-safe way to attempt to modify constant strings.
+What is needed is some way to say that \lstinline@s@'s type might contain qualifiers, and the result type has exactly the same qualifiers.
 Polymorphic functions do not provide a fix for this deficiency\index{deficiencies!pointers to qualified types}, because type qualifiers are not part of type values.
-Instead, overloading can be used to define \lstinline$strchr()$ for each combination of qualifiers.
+Instead, overloading can be used to define \lstinline@strchr()@ for each combination of qualifiers.
 \end{rationale}
 
@@ -3301 +3164 @@
 \end{lstlisting}
 Without this restriction, \CFA might require ``module initialization'' code ( since
-\lstinline$Rational$ has external linkage, it must be created before any other translation unit instantiates it), and would force an ordering on the initialization of the translation unit that defines \lstinline$Huge$ and the translation that declares \lstinline$Rational$.
+\lstinline@Rational@ has external linkage, it must be created before any other translation unit instantiates it), and would force an ordering on the initialization of the translation unit that defines \lstinline@Huge@ and the translation that declares \lstinline@Rational@.
 
 A benefit of the restriction is that it prevents the declaration in separate translation units of types that contain each other, which would be hard to prevent otherwise.
@@ -3318 +3181 @@
 \nonterm{struct-declaration}, type declarations can not be structure members.
 The form of
-\nonterm{type-declaration} forbids arrays of, pointers to, and functions returning \lstinline$type$.
+\nonterm{type-declaration} forbids arrays of, pointers to, and functions returning \lstinline@type@.
 Hence the syntax of \nonterm{type-specifier} does not have to be extended to allow type-valued expressions.
 It also side-steps the problem of type-valued expressions producing different values in different declarations.
@@ -3333 +3196 @@
 #include <stdlib.h>
 T * new( otype T ) { return ( T * )malloc( sizeof( T) ); };
-@\ldots@ int * ip = new( int );
-\end{lstlisting}
-This looks sensible, but \CFA's declaration-before-use rules mean that ``\lstinline$T$'' in the function body refers to the parameter, but the ``\lstinline$T$'' in the return type refers to the meaning of \lstinline$T$ in the scope that contains \lstinline$new$;
+§\ldots§ int * ip = new( int );
+\end{lstlisting}
+This looks sensible, but \CFA's declaration-before-use rules mean that ``\lstinline@T@'' in the function body refers to the parameter, but the ``\lstinline@T@'' in the return type refers to the meaning of \lstinline@T@ in the scope that contains \lstinline@new@;
 it could be undefined, or a type name, or a function or variable name.
 Nothing good can result from such a situation.
@@ -3352 +3215 @@
 f2( v2 );
 \end{lstlisting}
-\lstinline$V1$ is passed by value, so \lstinline$f1()$'s assignment to \lstinline$a[0]$ does not modify v1.  \lstinline$V2$ is converted to a pointer, so \lstinline$f2()$ modifies \lstinline$v2[0]$.
+\lstinline@V1@ is passed by value, so \lstinline@f1()@'s assignment to \lstinline@a[0]@ does not modify v1.  \lstinline@V2@ is converted to a pointer, so \lstinline@f2()@ modifies \lstinline@v2[0]@.
 
 A translation unit containing the declarations
 \begin{lstlisting}
-extern type Complex;@\use{Complex}@ // opaque type declaration
-extern float abs( Complex );@\use{abs}@
-\end{lstlisting} can contain declarations of complex numbers, which can be passed to \lstinline$abs$.
-Some other translation unit must implement \lstinline$Complex$ and \lstinline$abs$.
+extern type Complex;§\use{Complex}§ // opaque type declaration
+extern float abs( Complex );§\use{abs}§
+\end{lstlisting} can contain declarations of complex numbers, which can be passed to \lstinline@abs@.
+Some other translation unit must implement \lstinline@Complex@ and \lstinline@abs@.
 That unit might contain the declarations
 \begin{lstlisting}
-otype Complex = struct { float re, im; };@\impl{Complex}@
-Complex cplx_i = { 0.0, 1.0 };@\impl{cplx_i}@
-float abs( Complex c ) {@\impl{abs( Complex )}@
+otype Complex = struct { float re, im; };§\impl{Complex}§
+Complex cplx_i = { 0.0, 1.0 };§\impl{cplx_i}§
+float abs( Complex c ) {§\impl{abs( Complex )}§
         return sqrt( c.re * c.re + c.im * c.im );
 }
 \end{lstlisting}
-Note that \lstinline$c$ is implicitly converted to a \lstinline$struct$ so that its components can be retrieved.
-
-\begin{lstlisting}
-otype Time_of_day = int;@\impl{Time_of_day}@ // seconds since midnight. 
-Time_of_day ?+?( Time_of_day t1, int seconds ) {@\impl{?+?}@
+Note that \lstinline@c@ is implicitly converted to a \lstinline@struct@ so that its components can be retrieved.
+
+\begin{lstlisting}
+otype Time_of_day = int;§\impl{Time_of_day}§ // seconds since midnight. 
+Time_of_day ?+?( Time_of_day t1, int seconds ) {§\impl{?+?}§
         return (( int)t1 + seconds ) % 86400;
 }
 \end{lstlisting}
-\lstinline$t1$ must be cast to its implementation type to prevent infinite recursion.
+\lstinline@t1@ must be cast to its implementation type to prevent infinite recursion.
 
 \begin{rationale}
 Within the scope of a type definition, an instance of the type can be viewed as having that type or as having the implementation type.
-In the \lstinline$Time_of_day$ example, the difference is important.
+In the \lstinline@Time_of_day@ example, the difference is important.
 Different languages have treated the distinction between the abstraction and the implementation in different ways.
 \begin{itemize}
 \item
-Inside a Clu cluster \cite{clu}, the declaration of an instance states which view applies.
-Two primitives called \lstinline$up$ and \lstinline$down$ can be used to convert between the views.
-\item
-The Simula class \cite{Simula87} is essentially a record type.
+Inside a Clu cluster \cite{CLU}, the declaration of an instance states which view applies.
+Two primitives called \lstinline@up@ and \lstinline@down@ can be used to convert between the views.
+\item
+The Simula class \cite{SIMULA87} is essentially a record type.
 Since the only operations on a record are member selection and assignment, which can not be overloaded, there is never any ambiguity as to whether the abstraction or the implementation view is being used.
 In {\CC}
-\cite{c++}, operations on class instances include assignment and ``\lstinline$&$'', which can be overloaded.
+\cite{C++}, operations on class instances include assignment and ``\lstinline@&@'', which can be overloaded.
 A ``scope resolution'' operator can be used inside the class to specify whether the abstract or implementation version of the operation should be used.
 \item
-An Ada derived type definition \cite{ada} creates a new type from an old type, and also implicitly declares derived subprograms that correspond to the existing subprograms that use the old type as a parameter type or result type.
+An Ada derived type definition \cite{Ada} creates a new type from an old type, and also implicitly declares derived subprograms that correspond to the existing subprograms that use the old type as a parameter type or result type.
 The derived subprograms are clones of the existing subprograms with the old type replaced by the derived type.
 Literals and aggregates of the old type are also cloned.
@@ -3403 +3266 @@
 In this case, explicit conversions between the derived type and the old type can be used.
 \end{itemize}
-\CFA's rules are like Clu's, except that implicit conversions and conversion costs allow it to do away with most uses of \lstinline$up$ and \lstinline$down$. 
+\CFA's rules are like Clu's, except that implicit conversions and conversion costs allow it to do away with most uses of \lstinline@up@ and \lstinline@down@. 
 \end{rationale}
 
@@ -3409 +3272 @@
 \subsubsection{Default functions and objects}
 
-A declaration\index{type declaration} of a type identifier \lstinline$T$ with type-class
-\lstinline$type$ implicitly declares a \define{default assignment} function
-\lstinline$T ?=?( T *, T )$\use{?=?}, with the same \Index{scope} and \Index{linkage} as the identifier \lstinline$T$.
+A declaration\index{type declaration} of a type identifier \lstinline@T@ with type-class
+\lstinline@type@ implicitly declares a \define{default assignment} function
+\lstinline@T ?=?( T *, T )@\use{?=?}, with the same \Index{scope} and \Index{linkage} as the identifier \lstinline@T@.
 \begin{rationale}
 Assignment is central to C's imperative programming style, and every existing C object type has assignment defined for it ( except for array types, which are treated as pointer types for purposes of assignment).
 Without this rule, nearly every inferred type parameter would need an accompanying assignment assertion parameter.
 If a type parameter should not have an assignment operation,
-\lstinline$dtype$ should be used.
+\lstinline@dtype@ should be used.
 If a type should not have assignment defined, the user can define an assignment function that causes a run-time error, or provide an external declaration but no definition and thus cause a link-time error.
 \end{rationale}
 
-A definition\index{type definition} of a type identifier \lstinline$T$ with \Index{implementation type} \lstinline$I$ and type-class \lstinline$type$ implicitly defines a default assignment function.
-A definition\index{type definition} of a type identifier \lstinline$T$ with implementation type \lstinline$I$ and an assertion list implicitly defines \define{default function}s and
+A definition\index{type definition} of a type identifier \lstinline@T@ with \Index{implementation type} \lstinline@I@ and type-class \lstinline@type@ implicitly defines a default assignment function.
+A definition\index{type definition} of a type identifier \lstinline@T@ with implementation type \lstinline@I@ and an assertion list implicitly defines \define{default function}s and
 \define{default object}s as declared by the assertion declarations.
-The default objects and functions have the same \Index{scope} and \Index{linkage} as the identifier \lstinline$T$.
+The default objects and functions have the same \Index{scope} and \Index{linkage} as the identifier \lstinline@T@.
 Their values are determined as follows:
 \begin{itemize}
 \item
-If at the definition of \lstinline$T$ there is visible a declaration of an object with the same name as the default object, and if the type of that object with all occurrence of \lstinline$I$ replaced by \lstinline$T$ is compatible with the type of the default object, then the default object is initialized with that object.
-Otherwise the scope of the declaration of \lstinline$T$ must contain a definition of the default object.
+If at the definition of \lstinline@T@ there is visible a declaration of an object with the same name as the default object, and if the type of that object with all occurrence of \lstinline@I@ replaced by \lstinline@T@ is compatible with the type of the default object, then the default object is initialized with that object.
+Otherwise the scope of the declaration of \lstinline@T@ must contain a definition of the default object.
 
 \item 
-If at the definition of \lstinline$T$ there is visible a declaration of a function with the same name as the default function, and if the type of that function with all occurrence of \lstinline$I$ replaced by \lstinline$T$ is compatible with the type of the default function, then the default function calls that function after converting its arguments and returns the converted result.
-
-Otherwise, if \lstinline$I$ contains exactly one anonymous member\index{anonymous member} such that at the definition of \lstinline$T$ there is visible a declaration of a function with the same name as the default function, and the type of that function with all occurrences of the anonymous member's type in its parameter list replaced by \lstinline$T$ is compatible with the type of the default function, then the default function calls that function after converting its arguments and returns the result.
-
-Otherwise the scope of the declaration of \lstinline$T$ must contain a definition of the default function.
+If at the definition of \lstinline@T@ there is visible a declaration of a function with the same name as the default function, and if the type of that function with all occurrence of \lstinline@I@ replaced by \lstinline@T@ is compatible with the type of the default function, then the default function calls that function after converting its arguments and returns the converted result.
+
+Otherwise, if \lstinline@I@ contains exactly one anonymous member\index{anonymous member} such that at the definition of \lstinline@T@ there is visible a declaration of a function with the same name as the default function, and the type of that function with all occurrences of the anonymous member's type in its parameter list replaced by \lstinline@T@ is compatible with the type of the default function, then the default function calls that function after converting its arguments and returns the result.
+
+Otherwise the scope of the declaration of \lstinline@T@ must contain a definition of the default function.
 \end{itemize}
 \begin{rationale}
@@ -3441 +3304 @@
 \end{rationale}
 
-A function or object with the same type and name as a default function or object that is declared within the scope of the definition of \lstinline$T$ replaces the default function or object.
+A function or object with the same type and name as a default function or object that is declared within the scope of the definition of \lstinline@T@ replaces the default function or object.
 
 \examples
@@ -3451 +3314 @@
 Pair b = { 1, 1 };
 \end{lstlisting}
-The definition of \lstinline$Pair$ implicitly defines two objects \lstinline$a$ and \lstinline$b$.
-\lstinline$Pair a$ inherits its value from the \lstinline$struct impl a$.
+The definition of \lstinline@Pair@ implicitly defines two objects \lstinline@a@ and \lstinline@b@.
+\lstinline@Pair a@ inherits its value from the \lstinline@struct impl a@.
 The definition of
-\lstinline$Pair b$ is compulsory because there is no \lstinline$struct impl b$ to construct a value from.
+\lstinline@Pair b@ is compulsory because there is no \lstinline@struct impl b@ to construct a value from.
 \begin{lstlisting}
 trait ss( otype T ) {
@@ -3460 +3323 @@
         void munge( T * );
 }
-otype Whatsit | ss( Whatsit );@\use{Whatsit}@
-otype Doodad | ss( Doodad ) = struct doodad {@\use{Doodad}@
+otype Whatsit | ss( Whatsit );§\use{Whatsit}§
+otype Doodad | ss( Doodad ) = struct doodad {§\use{Doodad}§
         Whatsit; // anonymous member 
         int extra;
@@ -3467 +3330 @@
 Doodad clone( Doodad ) { ... }
 \end{lstlisting}
-The definition of \lstinline$Doodad$ implicitly defines three functions:
+The definition of \lstinline@Doodad@ implicitly defines three functions:
 \begin{lstlisting}
 Doodad ?=?( Doodad *, Doodad );
@@ -3473 +3336 @@
 void munge( Doodad * );
 \end{lstlisting}
-The assignment function inherits \lstinline$struct doodad$'s assignment function because the types match when \lstinline$struct doodad$ is replaced by \lstinline$Doodad$ throughout.
-\lstinline$munge()$ inherits \lstinline$Whatsit$'s \lstinline$munge()$ because the types match when
-\lstinline$Whatsit$ is replaced by \lstinline$Doodad$ in the parameter list. \lstinline$clone()$ does \emph{not} inherit \lstinline$Whatsit$'s \lstinline$clone()$: replacement in the parameter list yields ``\lstinline$Whatsit clone( Doodad )$'', which is not compatible with
-\lstinline$Doodad$'s \lstinline$clone()$'s type.
+The assignment function inherits \lstinline@struct doodad@'s assignment function because the types match when \lstinline@struct doodad@ is replaced by \lstinline@Doodad@ throughout.
+\lstinline@munge()@ inherits \lstinline@Whatsit@'s \lstinline@munge()@ because the types match when
+\lstinline@Whatsit@ is replaced by \lstinline@Doodad@ in the parameter list. \lstinline@clone()@ does \emph{not} inherit \lstinline@Whatsit@'s \lstinline@clone()@: replacement in the parameter list yields ``\lstinline@Whatsit clone( Doodad )@'', which is not compatible with
+\lstinline@Doodad@'s \lstinline@clone()@'s type.
 Hence the definition of
-``\lstinline$Doodad clone( Doodad )$'' is necessary.
+``\lstinline@Doodad clone( Doodad )@'' is necessary.
 
 Default functions and objects are subject to the normal scope rules.
 \begin{lstlisting}
-otype T = @\ldots@;
-T a_T = @\ldots@;               // Default assignment used. 
+otype T = §\ldots§;
+T a_T = §\ldots§;               // Default assignment used. 
 T ?=?( T *, T );
-T a_T = @\ldots@;               // Programmer-defined assignment called. 
+T a_T = §\ldots§;               // Programmer-defined assignment called. 
 \end{lstlisting}
 \begin{rationale}
@@ -3518 +3381 @@
 \begin{syntax}
 \oldlhs{labeled-statement}
-\rhs \lstinline$case$ \nonterm{case-value-list} : \nonterm{statement}
+\rhs \lstinline@case@ \nonterm{case-value-list} : \nonterm{statement}
 \lhs{case-value-list}
 \rhs \nonterm{case-value}
-\rhs \nonterm{case-value-list} \lstinline$,$ \nonterm{case-value}
+\rhs \nonterm{case-value-list} \lstinline@,@ \nonterm{case-value}
 \lhs{case-value}
 \rhs \nonterm{constant-expression}
 \rhs \nonterm{subrange}
 \lhs{subrange}
-\rhs \nonterm{constant-expression} \lstinline$~$ \nonterm{constant-expression}
+\rhs \nonterm{constant-expression} \lstinline@~@ \nonterm{constant-expression}
 \end{syntax}
 
@@ -3539 +3402 @@
 case 1~4, 9~14, 27~32:
 \end{lstlisting}
-The \lstinline$case$ and \lstinline$default$ clauses are restricted within the \lstinline$switch$ and \lstinline$choose$ statements, precluding Duff's device.
+The \lstinline@case@ and \lstinline@default@ clauses are restricted within the \lstinline@switch@ and \lstinline@choose@ statements, precluding Duff's device.
 
 
 \subsection{Expression and null statements}
 
-The expression in an expression statement is treated as being cast to \lstinline$void$.
+The expression in an expression statement is treated as being cast to \lstinline@void@.
 
 
@@ -3551 +3414 @@
 \begin{syntax}
 \oldlhs{selection-statement}
-\rhs \lstinline$choose$ \lstinline$($ \nonterm{expression} \lstinline$)$ \nonterm{statement}
+\rhs \lstinline@choose@ \lstinline@(@ \nonterm{expression} \lstinline@)@ \nonterm{statement}
 \end{syntax}
 
-The controlling expression \lstinline$E$ in the \lstinline$switch$ and \lstinline$choose$ statement:
+The controlling expression \lstinline@E@ in the \lstinline@switch@ and \lstinline@choose@ statement:
 \begin{lstlisting}
 switch ( E ) ...
@@ -3560 +3423 @@
 \end{lstlisting} may have more than one interpretation, but it shall have only one interpretation with an integral type.
 An \Index{integer promotion} is performed on the expression if necessary.
-The constant expressions in \lstinline$case$ statements with the switch are converted to the promoted type.
+The constant expressions in \lstinline@case@ statements with the switch are converted to the promoted type.
 
 
 \setcounter{subsubsection}{3}
-\subsubsection{The \lstinline$choose$ statement}
-
-The \lstinline$choose$ statement is the same as the \lstinline$switch$ statement except control transfers to the end of the \lstinline$choose$ statement at a \lstinline$case$ or \lstinline$default$ labeled statement.
-The \lstinline$fallthru$ statement is used to fall through to the next \lstinline$case$ or \lstinline$default$ labeled statement.
+\subsubsection[The choose statement]{The \lstinline@choose@ statement}
+
+The \lstinline@choose@ statement is the same as the \lstinline@switch@ statement except control transfers to the end of the \lstinline@choose@ statement at a \lstinline@case@ or \lstinline@default@ labeled statement.
+The \lstinline@fallthru@ statement is used to fall through to the next \lstinline@case@ or \lstinline@default@ labeled statement.
 The following have identical meaning:
 \begin{flushleft}
@@ -3592 +3455 @@
 \end{tabular}
 \end{flushleft}
-The \lstinline$choose$ statement addresses the problem of accidental fall-through associated with the \lstinline$switch$ statement.
+The \lstinline@choose@ statement addresses the problem of accidental fall-through associated with the \lstinline@switch@ statement.
 
 
 \subsection{Iteration statements}
 
-The controlling expression \lstinline$E$ in the loops
+The controlling expression \lstinline@E@ in the loops
 \begin{lstlisting}
 if ( E ) ...
 while ( E ) ...
 do ... while ( E );
-\end{lstlisting} is treated as ``\lstinline$( int )((E)!=0)$''.
+\end{lstlisting} is treated as ``\lstinline@( int )((E)!=0)@''.
 
 The statement 
 \begin{lstlisting}
-for ( a; b; c ) @\ldots@
+for ( a; b; c ) §\ldots§
 \end{lstlisting} is treated as
 \begin{lstlisting}
@@ -3617 +3480 @@
 \begin{syntax}
 \oldlhs{jump-statement}
-\rhs \lstinline$continue$ \nonterm{identifier}\opt
-\rhs \lstinline$break$ \nonterm{identifier}\opt
+\rhs \lstinline@continue@ \nonterm{identifier}\opt
+\rhs \lstinline@break@ \nonterm{identifier}\opt
 \rhs \ldots
-\rhs \lstinline$throw$ \nonterm{assignment-expression}\opt
-\rhs \lstinline$throwResume$ \nonterm{assignment-expression}\opt \nonterm{at-expression}\opt
-\lhs{at-expression} \lstinline$_At$ \nonterm{assignment-expression}
+\rhs \lstinline@throw@ \nonterm{assignment-expression}\opt
+\rhs \lstinline@throwResume@ \nonterm{assignment-expression}\opt \nonterm{at-expression}\opt
+\lhs{at-expression} \lstinline@_At@ \nonterm{assignment-expression}
 \end{syntax}
 
-Labeled \lstinline$continue$ and \lstinline$break$ allow useful but restricted control-flow that reduces the need for the \lstinline$goto$ statement for exiting multiple nested control-structures.
+Labeled \lstinline@continue@ and \lstinline@break@ allow useful but restricted control-flow that reduces the need for the \lstinline@goto@ statement for exiting multiple nested control-structures.
 \begin{lstlisting}
 L1: {                                                   // compound
@@ -3652 +3515 @@
 
 \setcounter{subsubsection}{1}
-\subsubsection{The \lstinline$continue$ statement}
-
-The identifier in a \lstinline$continue$ statement shall name a label located on an enclosing iteration statement.
-
-
-\subsubsection{The \lstinline$break$ statement}
-
-The identifier in a \lstinline$break$ statement shall name a label located on an enclosing compound, selection or iteration statement.
-
-
-\subsubsection{The \lstinline$return$ statement}
-
-An expression in a \lstinline$return$ statement is treated as being cast to the result type of the function.
-
-
-\subsubsection{The \lstinline$throw$ statement}
+\subsubsection[The continue statement]{The \lstinline@continue@ statement}
+
+The identifier in a \lstinline@continue@ statement shall name a label located on an enclosing iteration statement.
+
+
+\subsubsection[The break statement]{The \lstinline@break@ statement}
+
+The identifier in a \lstinline@break@ statement shall name a label located on an enclosing compound, selection or iteration statement.
+
+
+\subsubsection[The return statement]{The \lstinline@return@ statement}
+
+An expression in a \lstinline@return@ statement is treated as being cast to the result type of the function.
+
+
+\subsubsection[The throw statement]{The \lstinline@throw@ statement}
 
 When an exception is raised, \Index{propagation} directs control from a raise in the source execution to a handler in the faulting execution.
 
 
-\subsubsection{The \lstinline$throwResume$ statement}
+\subsubsection[The throwResume statement]{The \lstinline@throwResume@ statement}
 
 
@@ -3679 +3542 @@
 \begin{syntax}
 \lhs{exception-statement}
-\rhs \lstinline$try$ \nonterm{compound-statement} \nonterm{handler-list}
-\rhs \lstinline$try$ \nonterm{compound-statement} \nonterm{finally-clause}
-\rhs \lstinline$try$ \nonterm{compound-statement} \nonterm{handler-list} \nonterm{finally-clause}
+\rhs \lstinline@try@ \nonterm{compound-statement} \nonterm{handler-list}
+\rhs \lstinline@try@ \nonterm{compound-statement} \nonterm{finally-clause}
+\rhs \lstinline@try@ \nonterm{compound-statement} \nonterm{handler-list} \nonterm{finally-clause}
 \lhs{handler-list}
 \rhs \nonterm{handler-clause}
-\rhs \lstinline$catch$ \lstinline$($ \ldots \lstinline$)$ \nonterm{compound-statement}
-\rhs \nonterm{handler-clause} \lstinline$catch$ \lstinline$($ \ldots \lstinline$)$ \nonterm{compound-statement}
-\rhs \lstinline$catchResume$ \lstinline$($ \ldots \lstinline$)$ \nonterm{compound-statement}
-\rhs \nonterm{handler-clause} \lstinline$catchResume$ \lstinline$($ \ldots \lstinline$)$ \nonterm{compound-statement}
+\rhs \lstinline@catch@ \lstinline@(@ \ldots \lstinline@)@ \nonterm{compound-statement}
+\rhs \nonterm{handler-clause} \lstinline@catch@ \lstinline@(@ \ldots \lstinline@)@ \nonterm{compound-statement}
+\rhs \lstinline@catchResume@ \lstinline@(@ \ldots \lstinline@)@ \nonterm{compound-statement}
+\rhs \nonterm{handler-clause} \lstinline@catchResume@ \lstinline@(@ \ldots \lstinline@)@ \nonterm{compound-statement}
 \lhs{handler-clause}
-\rhs \lstinline$catch$ \lstinline$($ \nonterm{exception-declaration} \lstinline$)$ \nonterm{compound-statement}
-\rhs \nonterm{handler-clause} \lstinline$catch$ \lstinline$($ \nonterm{exception-declaration} \lstinline$)$ \nonterm{compound-statement}
-\rhs \lstinline$catchResume$ \lstinline$($ \nonterm{exception-declaration} \lstinline$)$ \nonterm{compound-statement}
-\rhs \nonterm{handler-clause} \lstinline$catchResume$ \lstinline$($ \nonterm{exception-declaration} \lstinline$)$ \nonterm{compound-statement}
+\rhs \lstinline@catch@ \lstinline@(@ \nonterm{exception-declaration} \lstinline@)@ \nonterm{compound-statement}
+\rhs \nonterm{handler-clause} \lstinline@catch@ \lstinline@(@ \nonterm{exception-declaration} \lstinline@)@ \nonterm{compound-statement}
+\rhs \lstinline@catchResume@ \lstinline@(@ \nonterm{exception-declaration} \lstinline@)@ \nonterm{compound-statement}
+\rhs \nonterm{handler-clause} \lstinline@catchResume@ \lstinline@(@ \nonterm{exception-declaration} \lstinline@)@ \nonterm{compound-statement}
 \lhs{finally-clause}
-\rhs \lstinline$finally$ \nonterm{compound-statement}
+\rhs \lstinline@finally@ \nonterm{compound-statement}
 \lhs{exception-declaration}
 \rhs \nonterm{type-specifier}
@@ -3702 +3565 @@
 \rhs \nonterm{new-abstract-declarator-tuple}
 \lhs{asynchronous-statement}
-\rhs \lstinline$enable$ \nonterm{identifier-list} \nonterm{compound-statement}
-\rhs \lstinline$disable$ \nonterm{identifier-list} \nonterm{compound-statement}
+\rhs \lstinline@enable@ \nonterm{identifier-list} \nonterm{compound-statement}
+\rhs \lstinline@disable@ \nonterm{identifier-list} \nonterm{compound-statement}
 \end{syntax}
 
@@ -3709 +3572 @@
 
 
-\subsubsection{The \lstinline$try$ statement}
-
-The \lstinline$try$ statement is a block with associated handlers, called a \Index{guarded block};
+\subsubsection[The try statement]{The \lstinline@try@ statement}
+
+The \lstinline@try@ statement is a block with associated handlers, called a \Index{guarded block};
 all other blocks are \Index{unguarded block}s.
-A \lstinline$goto$, \lstinline$break$, \lstinline$return$, or \lstinline$continue$ statement can be used to transfer control out of a try block or handler, but not into one.
-
-
-\subsubsection{The \lstinline$enable$/\lstinline$disable$ statements}
-
-The \lstinline$enable$/\lstinline$disable$ statements toggle delivery of \Index{asynchronous exception}s.
+A \lstinline@goto@, \lstinline@break@, \lstinline@return@, or \lstinline@continue@ statement can be used to transfer control out of a try block or handler, but not into one.
+
+
+\subsubsection[The enable/disable statements]{The \lstinline@enable@/\lstinline@disable@ statements}
+
+The \lstinline@enable@/\lstinline@disable@ statements toggle delivery of \Index{asynchronous exception}s.
 
 
@@ -3728 +3591 @@
 \subsection{Predefined macro names}
 
-The implementation shall define the macro names \lstinline$__LINE__$, \lstinline$__FILE__$,
-\lstinline$__DATE__$, and \lstinline$__TIME__$, as in the {\c11} standard.
-It shall not define the macro name \lstinline$__STDC__$.
-
-In addition, the implementation shall define the macro name \lstinline$__CFORALL__$ to be the decimal constant 1.
+The implementation shall define the macro names \lstinline@__LINE__@, \lstinline@__FILE__@,
+\lstinline@__DATE__@, and \lstinline@__TIME__@, as in the {\c11} standard.
+It shall not define the macro name \lstinline@__STDC__@.
+
+In addition, the implementation shall define the macro name \lstinline@__CFORALL__@ to be the decimal constant 1.
 
 
@@ -3749 +3612 @@
 The pointer, integral, and floating-point types are all \define{scalar types}.
 All of these types can be logically negated and compared.
-The assertion ``\lstinline$scalar( Complex )$'' should be read as ``type \lstinline$Complex$ is scalar''.
-\begin{lstlisting}
-trait scalar( otype T ) {@\impl{scalar}@
+The assertion ``\lstinline@scalar( Complex )@'' should be read as ``type \lstinline@Complex@ is scalar''.
+\begin{lstlisting}
+trait scalar( otype T ) {§\impl{scalar}§
         int !?( T );
         int ?<?( T, T ), ?<=?( T, T ), ?==?( T, T ), ?>=?( T, T ), ?>?( T, T ), ?!=?( T, T );
@@ -3761 +3624 @@
 This is equivalent to inheritance of specifications.
 \begin{lstlisting}
-trait arithmetic( otype T | scalar( T ) ) {@\impl{arithmetic}@@\use{scalar}@
+trait arithmetic( otype T | scalar( T ) ) {§\impl{arithmetic}§§\use{scalar}§
         T +?( T ), -?( T );
         T ?*?( T, T ), ?/?( T, T ), ?+?( T, T ), ?-?( T, T );
@@ -3767 +3630 @@
 \end{lstlisting}
 
-The various flavors of \lstinline$char$ and \lstinline$int$ and the enumerated types make up the
+The various flavors of \lstinline@char@ and \lstinline@int@ and the enumerated types make up the
 \define{integral types}.
 \begin{lstlisting}
-trait integral( otype T | arithmetic( T ) ) {@\impl{integral}@@\use{arithmetic}@
+trait integral( otype T | arithmetic( T ) ) {§\impl{integral}§§\use{arithmetic}§
         T ~?( T );
         T ?&?( T, T ), ?|?( T, T ), ?^?( T, T );
@@ -3784 +3647 @@
 The only operation that can be applied to all modifiable lvalues is simple assignment.
 \begin{lstlisting}
-trait m_lvalue( otype T ) {@\impl{m_lvalue}@
+trait m_lvalue( otype T ) {§\impl{m_lvalue}§
         T ?=?( T *, T );
 };
@@ -3794 +3657 @@
 Scalars can also be incremented and decremented.
 \begin{lstlisting}
-trait m_l_scalar( otype T | scalar( T ) | m_lvalue( T ) ) {@\impl{m_l_scalar}@
-        T ?++( T * ), ?--( T * );@\use{scalar}@@\use{m_lvalue}@
+trait m_l_scalar( otype T | scalar( T ) | m_lvalue( T ) ) {§\impl{m_l_scalar}§
+        T ?++( T * ), ?--( T * );§\use{scalar}§§\use{m_lvalue}§
         T ++?( T * ), --?( T * );
 };
@@ -3801 +3664 @@
 
 Modifiable arithmetic lvalues are both modifiable scalar lvalues and arithmetic.
-Note that this results in the ``inheritance'' of \lstinline$scalar$ along both paths.
-\begin{lstlisting}
-trait m_l_arithmetic( otype T | m_l_scalar( T ) | arithmetic( T ) ) {@\impl{m_l_arithmetic}@
-        T ?/=?( T *, T ), ?*=?( T *, T );@\use{m_l_scalar}@@\use{arithmetic}@
+Note that this results in the ``inheritance'' of \lstinline@scalar@ along both paths.
+\begin{lstlisting}
+trait m_l_arithmetic( otype T | m_l_scalar( T ) | arithmetic( T ) ) {§\impl{m_l_arithmetic}§
+        T ?/=?( T *, T ), ?*=?( T *, T );§\use{m_l_scalar}§§\use{arithmetic}§
         T ?+=?( T *, T ), ?-=?( T *, T );
 };
-trait m_l_integral( otype T | m_l_arithmetic( T ) | integral( T ) ) {@\impl{m_l_integral}@
-        T ?&=?( T *, T ), ?|=?( T *, T ), ?^=?( T *, T );@\use{m_l_arithmetic}@
-        T ?%=?( T *, T ), ?<<=?( T *, T ), ?>>=?( T *, T );@\use{integral}@
+trait m_l_integral( otype T | m_l_arithmetic( T ) | integral( T ) ) {§\impl{m_l_integral}§
+        T ?&=?( T *, T ), ?|=?( T *, T ), ?^=?( T *, T );§\use{m_l_arithmetic}§
+        T ?%=?( T *, T ), ?<<=?( T *, T ), ?>>=?( T *, T );§\use{integral}§
 };
 \end{lstlisting}
@@ -3817 +3680 @@
 
 Array types can barely be said to exist in {\c11}, since in most cases an array name is treated as a constant pointer to the first element of the array, and the subscript expression
-``\lstinline$a[i]$'' is equivalent to the dereferencing expression ``\lstinline$(*( a+( i )))$''.
-Technically, pointer arithmetic and pointer comparisons other than ``\lstinline$==$'' and
-``\lstinline$!=$'' are only defined for pointers to array elements, but the type system does not enforce those restrictions.
+``\lstinline@a[i]@'' is equivalent to the dereferencing expression ``\lstinline@(*( a+( i )))@''.
+Technically, pointer arithmetic and pointer comparisons other than ``\lstinline@==@'' and
+``\lstinline@!=@'' are only defined for pointers to array elements, but the type system does not enforce those restrictions.
 Consequently, there is no need for a separate ``array type'' specification.
 
 Pointer types are scalar types.
-Like other scalar types, they have ``\lstinline$+$'' and
-``\lstinline$-$'' operators, but the types do not match the types of the operations in
-\lstinline$arithmetic$, so these operators cannot be consolidated in \lstinline$scalar$.
-\begin{lstlisting}
-trait pointer( type P | scalar( P ) ) {@\impl{pointer}@@\use{scalar}@
+Like other scalar types, they have ``\lstinline@+@'' and
+``\lstinline@-@'' operators, but the types do not match the types of the operations in
+\lstinline@arithmetic@, so these operators cannot be consolidated in \lstinline@scalar@.
+\begin{lstlisting}
+trait pointer( type P | scalar( P ) ) {§\impl{pointer}§§\use{scalar}§
         P ?+?( P, long int ), ?+?( long int, P ), ?-?( P, long int );
         ptrdiff_t ?-?( P, P );
 };
-trait m_l_pointer( type P | pointer( P ) | m_l_scalar( P ) ) {@\impl{m_l_pointer}@
+trait m_l_pointer( type P | pointer( P ) | m_l_scalar( P ) ) {§\impl{m_l_pointer}§
         P ?+=?( P *, long int ), ?-=?( P *, long int );
         P ?=?( P *, void * );
@@ -3840 +3703 @@
 Specifications that define the dereference operator ( or subscript operator ) require two parameters, one for the pointer type and one for the pointed-at ( or element ) type.
 Different specifications are needed for each set of \Index{type qualifier}s, because qualifiers are not included in types.
-The assertion ``\lstinline$|ptr_to( Safe_pointer, int )$'' should be read as
-``\lstinline$Safe_pointer$ acts like a pointer to \lstinline$int$''.
-\begin{lstlisting}
-trait ptr_to( type P | pointer( P ), otype T ) {@\impl{ptr_to}@@\use{pointer}@
+The assertion ``\lstinline@|ptr_to( Safe_pointer, int )@'' should be read as
+``\lstinline@Safe_pointer@ acts like a pointer to \lstinline@int@''.
+\begin{lstlisting}
+trait ptr_to( otype P | pointer( P ), otype T ) {§\impl{ptr_to}§§\use{pointer}§
         lvalue T *?( P );
         lvalue T ?[?]( P, long int );
 };
-trait ptr_to_const( type P | pointer( P ), otype T ) {@\impl{ptr_to_const}@
+trait ptr_to_const( otype P | pointer( P ), otype T ) {§\impl{ptr_to_const}§
         const lvalue T *?( P );
-        const lvalue T ?[?]( P, long int );@\use{pointer}@
+        const lvalue T ?[?]( P, long int );§\use{pointer}§
 };
-trait ptr_to_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_volatile}@
+trait ptr_to_volatile( otype P | pointer( P ), otype T ) }§\impl{ptr_to_volatile}§
         volatile lvalue T *?( P );
-        volatile lvalue T ?[?]( P, long int );@\use{pointer}@
+        volatile lvalue T ?[?]( P, long int );§\use{pointer}§
 };
-trait ptr_to_const_volatile( type P | pointer( P ), otype T ) }@\impl{ptr_to_const_volatile}@
-        const volatile lvalue T *?( P );@\use{pointer}@
+trait ptr_to_const_volatile( otype P | pointer( P ), otype T ) }§\impl{ptr_to_const_volatile}§
+        const volatile lvalue T *?( P );§\use{pointer}§
         const volatile lvalue T ?[?]( P, long int );
 };
 \end{lstlisting}
 
-Assignment to pointers is more complicated than is the case with other types, because the target's type can have extra type qualifiers in the pointed-at type: a ``\lstinline$T *$'' can be assigned to a ``\lstinline$const T *$'', a ``\lstinline$volatile T *$'', and a ``\lstinline$const volatile T *$''.
+Assignment to pointers is more complicated than is the case with other types, because the target's type can have extra type qualifiers in the pointed-at type: a ``\lstinline@T *@'' can be assigned to a ``\lstinline@const T *@'', a ``\lstinline@volatile T *@'', and a ``\lstinline@const volatile T *@''.
 Again, the pointed-at type is passed in, so that assertions can connect these specifications to the
-``\lstinline$ptr_to$'' specifications.
-\begin{lstlisting}
-trait m_l_ptr_to( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to}@ otype T | ptr_to( P, T )@\use{ptr_to}@ {
+``\lstinline@ptr_to@'' specifications.
+\begin{lstlisting}
+trait m_l_ptr_to( otype P | m_l_pointer( P ),§\use{m_l_pointer}§§\impl{m_l_ptr_to}§ otype T | ptr_to( P, T )§\use{ptr_to}§ {
         P ?=?( P *, T * );
         T * ?=?( T **, P );
 };
-trait m_l_ptr_to_const( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_const}@ otype T | ptr_to_const( P, T )@\use{ptr_to_const}@) {
+trait m_l_ptr_to_const( otype P | m_l_pointer( P ),§\use{m_l_pointer}§§\impl{m_l_ptr_to_const}§ otype T | ptr_to_const( P, T )§\use{ptr_to_const}§) {
         P ?=?( P *, const T * );
         const T * ?=?( const T **, P );
 };
-trait m_l_ptr_to_volatile( type P | m_l_pointer( P ),@\use{m_l_pointer}@@\impl{m_l_ptr_to_volatile}@ otype T | ptr_to_volatile( P, T )) {@\use{ptr_to_volatile}@
+trait m_l_ptr_to_volatile( otype P | m_l_pointer( P ),§\use{m_l_pointer}§§\impl{m_l_ptr_to_volatile}§ otype T | ptr_to_volatile( P, T )) {§\use{ptr_to_volatile}§
         P ?=?( P *, volatile T * );
         volatile T * ?=?( volatile T **, P );
 };
-trait m_l_ptr_to_const_volatile( type P | ptr_to_const_volatile( P ),@\use{ptr_to_const_volatile}@@\impl{m_l_ptr_to_const_volatile}@
-                type T | m_l_ptr_to_volatile( P, T ) | m_l_ptr_to_const( P )) {@\use{m_l_ptr_to_const}@@\use{m_l_ptr_to_volatile}@
+trait m_l_ptr_to_const_volatile( otype P | ptr_to_const_volatile( P ),§\use{ptr_to_const_volatile}§§\impl{m_l_ptr_to_const_volatile}§
+                otype T | m_l_ptr_to_volatile( P, T ) | m_l_ptr_to_const( P )) {§\use{m_l_ptr_to_const}§§\use{m_l_ptr_to_volatile}§
         P ?=?( P *, const volatile T * );
         const volatile T * ?=?( const volatile T **, P );
@@ -3887 +3750 @@
 An alternative specification can make use of the fact that qualification of the pointed-at type is part of a pointer type to capture that regularity.
 \begin{lstlisting}
-trait m_l_ptr_like( type MyP | m_l_pointer( MyP ),@\use{m_l_pointer}@@\impl{m_l_ptr_like}@ type CP | m_l_pointer( CP ) ) {
+trait m_l_ptr_like( type MyP | m_l_pointer( MyP ),§\use{m_l_pointer}§§\impl{m_l_ptr_like}§ type CP | m_l_pointer( CP ) ) {
         MyP ?=?( MyP *, CP );
         CP ?=?( CP *, MyP );
 };
 \end{lstlisting}
-The assertion ``\lstinline$| m_l_ptr_like( Safe_ptr, const int * )$'' should be read as
-``\lstinline$Safe_ptr$ is a pointer type like \lstinline$const int *$''.
+The assertion ``\lstinline@| m_l_ptr_like( Safe_ptr, const int * )@'' should be read as
+``\lstinline@Safe_ptr@ is a pointer type like \lstinline@const int *@''.
 This specification has two defects, compared to the original four: there is no automatic assertion that dereferencing a
-\lstinline$MyP$ produces an lvalue of the type that \lstinline$CP$ points at, and the
-``\lstinline$|m_l_pointer( CP )$'' assertion provides only a weak assurance that the argument passed to \lstinline$CP$ really is a pointer type.
+\lstinline@MyP@ produces an lvalue of the type that \lstinline@CP@ points at, and the
+``\lstinline@|m_l_pointer( CP )@'' assertion provides only a weak assurance that the argument passed to \lstinline@CP@ really is a pointer type.
 
 
@@ -3902 +3765 @@
 
 Different operators often have related meanings;
-for instance, in C, ``\lstinline$+$'',
-``\lstinline$+=$'', and the two versions of ``\lstinline$++$'' perform variations of addition.
+for instance, in C, ``\lstinline@+@'',
+``\lstinline@+=@'', and the two versions of ``\lstinline@++@'' perform variations of addition.
 Languages like {\CC} and Ada allow programmers to define operators for new types, but do not require that these relationships be preserved, or even that all of the operators be implemented.
 Completeness and consistency is left to the good taste and discretion of the programmer.
@@ -3916 +3779 @@
 The different comparison operators have obvious relationships, but there is no obvious subset of the operations to use in the implementation of the others.
 However, it is usually convenient to implement a single comparison function that returns a negative integer, 0, or a positive integer if its first argument is respectively less than, equal to, or greater than its second argument;
-the library function \lstinline$strcmp$ is an example.
-
-C and \CFA have an extra, non-obvious comparison operator: ``\lstinline$!$'', logical negation, returns 1 if its operand compares equal to 0, and 0 otherwise.
+the library function \lstinline@strcmp@ is an example.
+
+C and \CFA have an extra, non-obvious comparison operator: ``\lstinline@!@'', logical negation, returns 1 if its operand compares equal to 0, and 0 otherwise.
 \begin{lstlisting}
 trait comparable( otype T ) {
@@ -3967 +3830 @@
 
 Note that, although an arithmetic type would certainly provide comparison functions, and an integral type would provide arithmetic operations, there does not have to be any relationship among
-\lstinline$int_base$, \lstinline$arith_base$ and \lstinline$comparable$.
+\lstinline@int_base@, \lstinline@arith_base@ and \lstinline@comparable@.
 Note also that these declarations provide guidance and assistance, but they do not define an absolutely minimal set of requirements.
-A truly minimal implementation of an arithmetic type might only provide
-\lstinline$0$, \lstinline$1$, and \lstinline$?-=?$, which would be used by polymorphic
-\lstinline$?+=?$, \lstinline$?*=?$, and \lstinline$?/=?$ functions.
-
-Note also that \lstinline$short$ is an integer type in C11 terms, but has no operations!
+A truly minimal implementation of an arithmetic type might only provide \lstinline@0@, \lstinline@1@, and \lstinline@?-=?@, which would be used by polymorphic \lstinline@?+=?@, \lstinline@?*=?@, and \lstinline@?/=?@ functions.
+
+Note also that \lstinline@short@ is an integer type in C11 terms, but has no operations!
 
 
@@ -3980 +3841 @@
 
 Restrict allowed to qualify anything, or type/dtype parameters, but only affects pointers.
-This gets into \lstinline$noalias$ territory.
-Qualifying anything (``\lstinline$short restrict rs$'') means pointer parameters of \lstinline$?++$, etc, would need restrict qualifiers.
+This gets into \lstinline@noalias@ territory.
+Qualifying anything (``\lstinline@short restrict rs@'') means pointer parameters of \lstinline@?++@, etc, would need restrict qualifiers.
 
 Enumerated types.
@@ -3991 +3852 @@
 Color, enum Color ) really make sense? ?++ does, but it adds (int)1.
 
-Operators on {,signed,unsigned} char and other small types. ?<? harmless;
+Operators on {,signed,unsigned} char and other small types. \lstinline@?<?@ harmless;
 ?*? questionable for chars.
 Generic selections make these choices visible.
@@ -3997 +3858 @@
 ``promotion'' function?
 
-\lstinline$register$ assignment might be handled as assignment to a temporary with copying back and forth, but copying must not be done by assignment.
-
-Don't use ptrdiff\_t by name in the predefineds.
+\lstinline@register@ assignment might be handled as assignment to a temporary with copying back and forth, but copying must not be done by assignment.
+
+Don't use \lstinline@ptrdiff_t@ by name in the predefineds.
 
 Polymorphic objects.
@@ -4006 +3867 @@
 
 \bibliographystyle{plain}
-\bibliography{refrat}
+\bibliography{cfa}
 
 

doc/user/Makefile

@@ -1 +1 @@
 ## Define the appropriate configuration variables.
 
-TeXLIB = .::
+TeXLIB = .:../bibliography/:../LaTeXmacros/:
 LaTeX  = TEXINPUTS=${TeXLIB} && export TEXINPUTS && latex
-BibTeX = BSTINPUTS=${TeXLIB} && export BSTINPUTS && bibtex
+BibTeX = BIBINPUTS=${TeXLIB} && export BIBINPUTS && bibtex
 
 ## Define the text source files.
@@ -12 +12 @@
 
 FIGURES = ${addsuffix .tex, \
+Cdecl \
 }
 
@@ -43 +44 @@
         dvips $< -o $@
 
-${basename ${DOCUMENT}}.dvi : Makefile ${GRAPHS} ${PROGRAMS} ${PICTURES} ${FIGURES} ${SOURCES} ${basename ${DOCUMENT}}.tex ${basename ${DOCUMENT}}.bib /usr/local/bibliographies/pl.bib
+${basename ${DOCUMENT}}.dvi : Makefile ${GRAPHS} ${PROGRAMS} ${PICTURES} ${FIGURES} ${SOURCES} ${basename ${DOCUMENT}}.tex \
+                ../LaTeXmacros/common.tex ../LaTeXmacros/indexstyle ../bibliography/cfa.bib
         # Conditionally create an empty *.ind (index) file for inclusion until makeindex is run.
         if [ ! -r ${basename $@}.ind ] ; then touch ${basename $@}.ind ; fi
@@ -53 +55 @@
         -${BibTeX} ${basename $@}
         # Make index from *.aux entries and input index at end of document
-        makeindex -s indexstyle ${basename $@}.idx
+        makeindex -s ../LaTeXmacros/indexstyle ${basename $@}.idx
         ${LaTeX} ${basename $@}.tex
         # Run again to get index title into table of contents

doc/user/user.tex

@@ +1 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- Mode: Latex -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% 
+%% Cforall Version 1.0.0 Copyright (C) 2016 University of Waterloo
+%%
+%% The contents of this file are covered under the licence agreement in the
+%% file "LICENCE" distributed with Cforall.
+%% 
+%% user.tex -- 
+%% 
+%% Author           : Peter A. Buhr
+%% Created On       : Wed Apr  6 14:53:29 2016
+%% Last Modified By : Peter A. Buhr
+%% Last Modified On : Sat Apr 30 13:54:32 2016
+%% Update Count     : 221
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 % requires tex packages: texlive-base texlive-latex-base tex-common texlive-humanities texlive-latex-extra texlive-fonts-recommended
+
+% red highlighting ®...® (registered trademark sumbol)
+% blue highlighting ©...© (copyright symbol)
+% latex escape §...§ (section symbol)
+% keyword escape ¶...¶ (pilcrow symbol)
+% math escape $...$ (dollar symbol)
 
 \documentclass[openright,twoside]{article}
@@ -5 +27 @@
 
 % Latex packages used in the document.
-
+\usepackage[T1]{fontenc}                                % allow Latin1 (extended ASCII) characters
+\usepackage{textcomp}
+\usepackage[latin1]{inputenc}
+\usepackage{upquote}
 \usepackage{fullpage,times}
+\usepackage{epic,eepic}
 \usepackage{xspace}
 \usepackage{varioref}
@@ -12 +38 @@
 \usepackage{footmisc}
 \usepackage{comment}
-\usepackage{latexsym}                                   % \Box
-\usepackage{mathptmx}                                   % better math font with "times"
+\usepackage{latexsym}                                   % \Box
+\usepackage{mathptmx}                                   % better math font with "times"
 \usepackage[pagewise]{lineno}
 \renewcommand{\linenumberfont}{\scriptsize\sffamily}
@@ -22 +48 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+% Bespoke macros used in the document.
+\input{common}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 % Names used in the document.
 
-\newcommand{\CFA}{C$\forall$\xspace}    % set language symbolic name
-\newcommand{\CFL}{Cforall\xspace}               % set language text name
-\newcommand{\CC}{C\kern-.1em\hbox{+\kern-.25em+}\xspace} % CC symbolic name
-\def\c11{ISO/IEC C} % C11 name (cannot have numbers in latex command name)
+\newcommand{\Version}{1.0.0}
 \newcommand{\CS}{C\raisebox{-0.9ex}{\large$^\sharp$}\xspace}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-% Bespoke macros used in the document.
-
-\makeatletter
-% allow escape sequence in lstinline
-%\usepackage{etoolbox}
-%\patchcmd{\lsthk@TextStyle}{\let\lst@DefEsc\@empty}{}{}{\errmessage{failed to patch}}
-
-\renewcommand\small{%
-   \@setfontsize\small{8.5}{11}%
-   \abovedisplayskip 8.5pt \@plus 3pt \@minus 4pt
-   \abovedisplayshortskip \z@ \@plus 2pt
-   \belowdisplayshortskip 4pt \@plus 2pt \@minus 2pt
-   \def\@listi{\leftmargin\leftmargini
-               \topsep 4pt \@plus 2pt \@minus 2pt
-               \parsep 2pt \@pluspt \@minuspt
-               \itemsep \parsep}%
-   \belowdisplayskip \abovedisplayskip
-}
-\usepackage{relsize}            % must be after change to small
-
-\renewcommand{\labelitemi}{{\raisebox{0.25ex}{\footnotesize$\bullet$}}}
-\renewenvironment{itemize}{\begin{list}{\labelitemi}{\topsep=5pt\itemsep=5pt\parsep=0pt}}{\end{list}}
-
-%  Reduce size of section titles
-\renewcommand\section{\@startsection{section}{1}{\z@}{-3.0ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\large\bfseries}}
-\renewcommand\subsection{\@startsection{subsection}{2}{\z@}{-2.5ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\normalsize\bfseries}}
-\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}{-2.5ex \@plus -1ex \@minus -.2ex}{1.0ex \@plus .2ex}{\normalfont\normalsize\bfseries}}
-\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}{-2.0ex \@plus -1ex \@minus -.2ex}{-1em}{\normalfont\normalsize\bfseries}}
-
-% index macros
-\newcommand{\italic}[1]{\emph{\hyperpage{#1}}}
-\newcommand{\definition}[1]{\textbf{\hyperpage{#1}}}
-\newcommand{\see}[1]{\emph{see} #1}
-
-% Define some commands that produce formatted index entries suitable for cross-references.
-% ``\spec'' produces entries for specifications of entities.  ``\impl'' produces entries for their
-% implementations, and ``\use'' for their uses.
-
-%  \newcommand{\bold}[1]{{\bf #1}}
-%  \def\spec{\@bsphack\begingroup
-%             \def\protect##1{\string##1\space}\@sanitize
-%             \@wrxref{|bold}}
-\def\impl{\@bsphack\begingroup
-          \def\protect##1{\string##1\space}\@sanitize
-          \@wrxref{|definition}}
-\newcommand{\indexcode}[1]{{\lstinline$#1$}}
-\def\use{\@bsphack\begingroup
-         \def\protect##1{\string##1\space}\@sanitize
-         \@wrxref{|hyperpage}}
-\def\@wrxref#1#2{\let\thepage\relax
-    \xdef\@gtempa{\write\@indexfile{\string
-    \indexentry{#2@{\lstinline$#2$}#1}{\thepage}}}\endgroup\@gtempa
-    \if@nobreak \ifvmode\nobreak\fi\fi\@esphack}
-%\newcommand{\use}[1]{\index{#1@{\lstinline$#1$}}}
-%\newcommand{\impl}[1]{\index{\protect#1@{\lstinline$\protect#1$}|definition}}
-
-% inline text and lowercase index: \Index{inline and lowercase index text}
-% inline text and as-in index: \Index[as-is index text]{inline text}
-% inline text but index with different as-is text: \Index[index text]{inline text}
-\newcommand{\Index}{\@ifstar\@sIndex\@Index}
-\newcommand{\@Index}[2][\@empty]{\lowercase{\def\temp{#2}}#2\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi}
-\newcommand{\@sIndex}[2][\@empty]{#2\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi}
-
-\newcommand{\newtermFontInline}{\emph}
-\newcommand{\newterm}{\@ifstar\@snewterm\@newterm}
-\newcommand{\@newterm}[2][\@empty]{\lowercase{\def\temp{#2}}{\newtermFontInline{#2}}\ifx#1\@empty\index{\temp}\else\index{#1@{\protect#2}}\fi}
-\newcommand{\@snewterm}[2][\@empty]{{\newtermFontInline{#2}}\ifx#1\@empty\index{#2}\else\index{#1@{\protect#2}}\fi}
-\makeatother
-
-% blocks and titles
-\newenvironment{quote2}{%
-        \list{}{\lstset{resetmargins=true}\leftmargin=\parindent\rightmargin\leftmargin}%
-        \item\relax
-}{%
-        \endlist
-}% quote2
-\newenvironment{rationale}{%
-  \begin{quotation}\noindent$\Box$\enspace
-}{%
-  \hfill\enspace$\Box$\end{quotation}
-}%
-\newcommand{\define}[1]{\emph{#1\/}\index{#1}}
-\newcommand{\rewrite}{\(\Rightarrow\)}
-\newcommand{\rewriterules}{\paragraph{Rewrite Rules}~\par\noindent}
-\newcommand{\examples}{\paragraph{Examples}~\par\noindent}
-\newcommand{\semantics}{\paragraph{Semantics}~\par\noindent}
-\newcommand{\constraints}{\paragraph{Constraints}~\par\noindent}
-\newcommand{\predefined}{\paragraph{Predefined Identifiers}~\par\noindent}
-
-% BNF macros
-\def\syntax{\paragraph{Syntax}\trivlist\parindent=.5in\item[\hskip.5in]}
-\let\endsyntax=\endtrivlist
-\newcommand{\lhs}[1]{\par{\emph{#1:}}\index{#1@{\emph{#1}}|italic}}
-\newcommand{\rhs}{\hfil\break\hbox{\hskip1in}}
-\newcommand{\oldlhs}[1]{\emph{#1: \ldots}\index{#1@{\emph{#1}}|italic}}
-\newcommand{\nonterm}[1]{\emph{#1\/}\index{#1@{\emph{#1}}|italic}}
-\newcommand{\opt}{$_{opt}$\ }
-
-% adjust varioref package with default "section" and "page" titles, and optional title with faraway page numbers
-% \VRef{label} => Section 2.7, \VPageref{label} => page 17
-% \VRef[Figure]{label} => Figure 3.4, \VPageref{label} => page 17
-\renewcommand{\reftextfaceafter}{\unskip}
-\renewcommand{\reftextfacebefore}{\unskip}
-\renewcommand{\reftextafter}{\unskip}
-\renewcommand{\reftextbefore}{\unskip}
-\renewcommand{\reftextfaraway}[1]{\unskip, p.~\pageref{#1}}
-\renewcommand{\reftextpagerange}[2]{\unskip, pp.~\pageref{#1}--\pageref{#2}}
-\newcommand{\VRef}[2][Section]{\ifx#1\@empty\else{#1}\nobreakspace\fi\vref{#2}}
-\newcommand{\VPageref}[2][page]{\ifx#1\@empty\else{#1}\nobreakspace\fi\pageref{#2}}
-
-% Go programming language
-\lstdefinelanguage{Golang}%
-  {morekeywords=[1]{package,import,func,type,struct,return,defer,panic, recover,select,var,const,iota,},%
-   morekeywords=[2]{string,uint,uint8,uint16,uint32,uint64,int,int8,int16, int32,int64,
-                bool,float32,float64,complex64,complex128,byte,rune,uintptr, error,interface},%
-   morekeywords=[3]{map,slice,make,new,nil,len,cap,copy,close,true,false, delete,append,real,imag,complex,chan,},%
-   morekeywords=[4]{for,break,continue,range,goto,switch,case,fallthrough,if, else,default,},%
-   morekeywords=[5]{Println,Printf,Error,},%
-   sensitive=true,%
-   morecomment=[l]{//},%
-   morecomment=[s]{/*}{*/},%
-   morestring=[b]',%
-   morestring=[b]",%
-   morestring=[s]{`}{`},%
-}
-
-% CFA based on ANSI C
-\lstdefinelanguage{CFA}[ANSI]{C}%
-{morekeywords={asm,_Alignas,_Alignof,_At,_Atomic,_Bool,catch,catchResume,choose,_Complex,trait,disable,dtype,enable,
-        fallthru,finally,forall,ftype,_Generic,_Imaginary,inline,lvalue,_Noreturn,otype,restrict,_Static_assert,
-        _Thread_local,throw,throwResume,try,},
-}%
-
-\lstset{
-language=CFA,
-columns=flexible,
-basicstyle=\sf\relsize{-1},
-tabsize=4,
-xleftmargin=\parindent,
-escapechar=@,
-mathescape=true,
-keepspaces=true,
-showstringspaces=false,
-showlines=true,
-}%
-
-\makeatletter
-% replace/adjust listings characters that look bad in sanserif
-\lst@CCPutMacro
-\lst@ProcessOther{"2D}{\lst@ttfamily{-{}}{{\ttfamily\upshape -}}} % replace minus
-\lst@ProcessOther{"3C}{\lst@ttfamily{<}{\texttt{<}}} % replace less than
-\lst@ProcessOther{"3E}{\lst@ttfamily{<}{\texttt{>}}} % replace greater than
-\lst@ProcessOther{"5E}{\raisebox{0.4ex}{$\scriptstyle\land\,$}} % replace circumflex
-\lst@ProcessLetter{"5F}{\lst@ttfamily{\char95}{{\makebox[1.2ex][c]{\rule{1ex}{0.1ex}}}}} % replace underscore
-\lst@ProcessOther{"7E}{\raisebox{0.3ex}{$\scriptstyle\sim\,$}} % replace tilde
-%\lst@ProcessOther{"7E}{\raisebox{-.4ex}[1ex][0pt]{\textasciitilde}} % lower tilde
-\@empty\z@\@empty
-\makeatother
-
-\setcounter{secnumdepth}{3}     % number subsubsections
-\setcounter{tocdepth}{3}                % subsubsections in table of contents
+\setcounter{secnumdepth}{3}                             % number subsubsections
+\setcounter{tocdepth}{3}                                % subsubsections in table of contents
 \makeindex
 
@@ -199 +68 @@
 \begin{document}
 \pagestyle{headings}
-\linenumbers                                    % comment out to turn off line numbering
+\linenumbers                                            % comment out to turn off line numbering
 
 \title{\Huge
@@ -213 +82 @@
 }% author
 \date{
-DRAFT\\\today
+DRAFT \\
+\today
 }% date
 
@@ -241 +111 @@
 
 \CFA\footnote{Pronounced ``C-for-all'', and written \CFA, CFA, or \CFL.} is a modern general-purpose programming-language, designed an as evolutionary step forward from the C programming language.
-The syntax of the \CFA language builds from that of C, and should look immediately familiar to C programmers.
+The syntax of the \CFA language builds from C, and should look immediately familiar to C programmers.
 % Any language feature that is not described here can be assumed to be using the standard C11 syntax.
-\CFA has added many modern programming-language features, which directly leads to increased safety and productivity, while maintaining interoperability with existing C programs, and maintaining C-like performance.
+\CFA adds many modern programming-language features, which directly leads to increased safety and productivity, while maintaining interoperability with existing C programs and achieving C performance.
 Like C, \CFA is a statically typed, procedural language with a low-overhead runtime, meaning there is no global garbage-collection.
 The primary new features include parametric-polymorphism routines and types, exceptions, concurrency, and modules.
@@ -254 +124 @@
 New programs can be written in \CFA using a combination of C and \CFA features.
 \CC had a similar goal 30 years ago, but has struggled over the intervening time to incorporate modern programming-language features because of early design choices.
-\CFA has 30 years of hindsight and a much cleaner starting point than \CC.
+\CFA has 30 years of hindsight and clean starting point.
 
 Like \CC, there may be both an old and new ways to achieve the same effect.
@@ -279 +149 @@
 \end{quote2}
 Both programs output the same result.
-While the \CFA I/O looks similar to the \CC style of output, there are several important differences, such as automatic spacing between variables as in Python (see also~\VRef{s:IOLibrary}).
+While the \CFA I/O looks similar to the \CC output style, there are several important differences, such as automatic spacing between variables as in Python (see also~\VRef{s:IOLibrary}).
 
 This document is a reference manual for the \CFA programming language, targeted at \CFA programmers.
-Implementers may also refer to the \CFA Programming Language Specification for details about the language syntax and semantics.
+Implementers may refer to the \CFA Programming Language Specification for details about the language syntax and semantics.
 In its current state, this document covers the intended core features of the language.
 Changes to the syntax and additional features are expected to be included in later revisions.
@@ -294 +164 @@
 The original \CFA project~\cite{Ditchfield92} extended the C type system with parametric polymorphism and overloading, as opposed to the \CC approach of object-oriented extensions to the C type-system.
 A first implementation of the core Cforall language was created~\cite{Bilson03,Esteves04}, but at the time there was little interesting in extending C, so work did not continue.
-As the saying goes, ``What goes around, comes around'', and there is now renewed interest in the C programming language, so the \CFA project has been restarted.
-
-
-\section{Motivation: Why fix C?}
+As the saying goes, ``What goes around, comes around'', and there is now renewed interest in the C programming language because of legacy code-bases, so the \CFA project has been restarted.
+
+
+\section{Why fix C?}
 
 Even with all its problems, C is a very popular programming language because it allows writing software at virtually any level in a computer system without restriction.
@@ -314 +184 @@
 Java~\cite{Java8}, Go~\cite{Go}, Rust~\cite{Rust} and D~\cite{D} are examples of the revolutionary approach for modernizing C/\CC, resulting in a new language rather than an extension of the descendent.
 These languages have different syntax and semantics from C, and do not interoperate directly with C, largely because of garbage collection.
-As a result, there is a significant learning curve to move to these languages, and C legacy-code must be complete rewritten.
+As a result, there is a significant learning curve to move to these languages, and C legacy-code must be rewritten.
 These costs can be prohibitive for many companies with a large software base in C/\CC, and many programmers that require retraining to a new programming language.
 
@@ -331 +201 @@
 This feature allows users of \CFA to take advantage of the existing panoply of C libraries from inside their \CFA code.
 In fact, one of the biggest issues for any new programming language is establishing a minimum level of library code to support a large body of activities.
-Programming-language developers often state that adequate library support costs many times more than designing and implementing the language itself.
+Programming-language developers often state that adequate library support takes more work than designing and implementing the language itself.
 Like \CC, \CFA starts with immediate access to all exiting C libraries, and in many cases, can easily wrap library routines with simpler and safer interfaces, at very low cost.
 
@@ -338 +208 @@
 Whereas, \CFA wraps each of these routines into one with the common name \lstinline@abs@.
 \begin{lstlisting}
+char abs( char );
 extern "C" {
-#include <stdlib.h>                     // provide C prototype for integer "abs" routine
+int abs( int );                         // use default C routine for int
 } // extern "C"
-
-char abs( char );
-long int abs( long int );       // @{\CFA}@ overload name "abs" for other types
+long int abs( long int );
 long long int abs( long long int );
 float abs( float );
@@ -360 +229 @@
 The name ``\lstinline@abs@'' evokes the notion of absolute value, and many mathematical types provide the notion of absolute value.
 Hence, knowing the name \lstinline@abs@ should be sufficient to apply it to any type where it is applicable.
-The time savings and safety of using one name uniformly versus @N@ unique names should not be underestimated.
-
-
-\section{Compiling \CFA}
+The time savings and safety of using one name uniformly versus $N$ unique names should not be underestimated.
+
+
+\section[Compiling CFA Program]{Compiling \CFA Program}
 
 The command \lstinline@cfa@ is used to compile \CFA program(s).
-This command works like the GNU \lstinline@gcc@ command, e.g.:
-\begin{lstlisting}
-cfa [ gcc-options ] C/@{\CFA}@-files [ assembler/loader-files ]
-\end{lstlisting}
-The following additional option is available:
+This command works like the GNU \lstinline@gcc@\index{gcc} command, e.g.:
+\begin{lstlisting}
+cfa [ gcc-options ] C/§\CFA§-files [ assembler/loader-files ]
+\end{lstlisting}
+\indexc{cfa}\index{compilation!cfa@\lstinline$cfa$}
+By default, \CFA programs having the following \lstinline@gcc@ flags turned on:
 \begin{description}
-\item
-\hspace*{-4pt}\lstinline@-CFA@
+\item\hspace*{-4pt}\Indexc{-std=gnu99}\index{compilation option!-std=gnu99@{\lstinline$-std=gnu99$}}
+The 1999 C standard plus GNU extensions.
+\item\hspace*{-4pt}\Indexc{-fgnu89-¶inline¶}\index{compilation option!-fgnu89-inline@{\lstinline$-fgnu89-¶inline¶$}}
+Use the traditional GNU semantics for inline routines in C99 mode.
+\end{description}
+The following new \CFA option is available:
+\begin{description}
+\item\hspace*{-4pt}\Indexc{-CFA}\index{compilation option!-CFA@{\lstinline$-CFA$}}
 Only the C preprocessor and the \CFA translator steps are performed and the transformed program is written to standard output, which makes it possible to examine the code generated by the \CFA translator.
 \end{description}
 
+The following preprocessor variables are available:
+\begin{description}
+\item\hspace*{-4pt}\Indexc{__CFA__}\index{preprocessor variables!__CFA__@{\lstinline$__CFA__$}}
+is always available during preprocessing and its value is the current major \Index{version number} of \CFA.\footnote{
+The C preprocessor allows only integer values in a preprocessor variable so a value like ``\Version'' is not allowed.
+Hence, the need to have three variables for the major, minor and patch version number.}
+
+\item\hspace*{-4pt}\Indexc{__CFA_MINOR__}\index{preprocessor variables!__CFA_MINOR__@{\lstinline$__CFA_MINOR__$}}
+is always available during preprocessing and its value is the current minor \Index{version number} of \CFA.
+
+\item\hspace*{-4pt}\Indexc{__CFA_PATCH__}\index{preprocessor variables!__CFA_PATCH__@\lstinline$__CFA_PATCH__$}
+is always available during preprocessing and its value is the current patch \Index{version number} of \CFA.
+
+\item\hspace*{-4pt}\Indexc{__CFORALL__}\index{preprocessor variables!__CFORALL__@\lstinline$__CFORALL__$}
+is always available during preprocessing and it has no value.
+\end{description}
+
+These preprocessor variables allow conditional compilation of programs that must work differently in these situations.
+For example, to toggle between C and \CFA extensions, using the following:
+\begin{lstlisting}
+#ifndef __CFORALL__
+#include <stdio.h>                      // C header file
+#else
+#include <fstream>                      // §\CFA{}§ header file
+#endif
+\end{lstlisting}
+which conditionally includes the correct header file, if the program is compiled using \lstinline@gcc@ or \lstinline@cfa@. 
+
 
 \section{Underscores in Constants}
@@ -382 +286 @@
 Numeric constants are extended to allow \Index{underscore}s within constants\index{constant!underscore}, e.g.:
 \begin{lstlisting}
-2_147_483_648;                          // decimal constant
+2®_®147®_®483®_®648;                            // decimal constant
 56_ul;                                          // decimal unsigned long constant
 0_377;                                          // octal constant
@@ -408 +312 @@
 the type suffixes \lstinline@U@, \lstinline@L@, etc. may start with an underscore \lstinline@1_U@, \lstinline@1_ll@ or \lstinline@1.0E10_f@.
 \end{enumerate}
-It is significantly easier to read and type long constants when they are broken up into smaller groupings (most cultures use comma or period among digits for the same purpose).
+It is significantly easier to read and enter long constants when they are broken up into smaller groupings (most cultures use comma or period among digits for the same purpose).
 This extension is backwards compatible, matches with the use of underscore in variable names, and appears in Ada and Java.
 
@@ -417 +321 @@
 C declaration syntax is notoriously confusing and error prone.
 For example, many C programmers are confused by a declaration as simple as:
-\begin{lstlisting}
-int *x[ 10 ]
-\end{lstlisting}
-Is this a pointer to an array of 10 integers or an array of 10 pointers to integers?
+\begin{quote2}
+\begin{tabular}{@{}ll@{}}
+\begin{lstlisting}[aboveskip=0pt,belowskip=0pt]
+int *x[ 5 ]
+\end{lstlisting}
+&
+\raisebox{-0.75\totalheight}{\input{Cdecl}}
+\end{tabular}
+\end{quote2}
+Is this an array of 5 pointers to integers or a pointer to an array of 5 integers?
 Another example of confusion results from the fact that a routine name and its parameters are embedded within the return type, mimicking the way the return value is used at the routine's call site.
 For example, a routine returning a pointer to an array of integers is defined and used in the following way:
 \begin{lstlisting}
-int (*f())[ 10 ] {...};
-... (*f())[ 3 ] += 1;           // definition mimics usage
+int (*f())[ 5 ] {...};  // definition mimics usage
+... (*f())[ 3 ] += 1;
 \end{lstlisting}
 Essentially, the return type is wrapped around the routine name in successive layers (like an onion).
@@ -434 +344 @@
 The only exception is bit field specification, which always appear to the right of the base type.
 C and the new \CFA declarations may appear together in the same program block, but cannot be mixed within a specific declaration.
-Unsupported are K\&R C declarations where the base type defaults to \lstinline@int@, if no type is specified\footnote{
-At least one type specifier shall be given in the declaration specifiers in each declaration, and in the specifier-qualifier list in each structure declaration and type name~\cite[\S~6.7.2(2)]{C11}},
-e.g.:
-\begin{lstlisting}
-x;                                      // int x
-*y;                                     // int *y
-f( p1, p2 );            // int f( int p1, int p2 );
-f( p1, p2 ) {}          // int f( int p1, int p2 ) {}
-\end{lstlisting}
 
 In \CFA declarations, the same tokens are used as in C: the character \lstinline@*@ is used to indicate a pointer, square brackets \lstinline@[@\,\lstinline@]@ are used to represent an array, and parentheses \lstinline@()@ are used to indicate a routine parameter.
@@ -451 +352 @@
 \multicolumn{1}{c@{\hspace{30pt}}}{\textbf{\CFA}}       & \multicolumn{1}{c}{\textbf{C}}        \\
 \begin{lstlisting}
-* int x, y;
+®* int x, y;®
 \end{lstlisting}
 &
@@ -464 +365 @@
 \multicolumn{1}{c@{\hspace{30pt}}}{\textbf{\CFA}}       & \multicolumn{1}{c@{\hspace{20pt}}}{\textbf{C}}        \\
 \begin{lstlisting}
-[ 10 ] int z;
-[ 10 ] * char w;
-* [ 10 ] double v;
+[ 5 ] int z;
+[ 5 ] * char w;
+* [ 5 ] double v;
 struct s {
-int f0:3;
+        int f0:3;
         * int f1;
-        [ 10 ] * int f2;
+        [ 5 ] * int f2;
 };
 \end{lstlisting}
 &
 \begin{lstlisting}
-int z[ 10 ];
-char *w[ 10 ];
-double (*v)[ 10 ];
+int z[ 5 ];
+char *w[ 5 ];
+double (*v)[ 5 ];
 struct s {
         int f0:3;
         int *f1;
-        int *f2[ 10 ]
+        int *f2[ 5 ]
 };
 \end{lstlisting}
 &
 \begin{lstlisting}
-// array of 10 integers
-// array of 10 pointers to char
-// pointer to array of 10 doubles
+// array of 5 integers
+// array of 5 pointers to char
+// pointer to array of 5 doubles
 
 // common bit field syntax
@@ -497 +398 @@
 \end{tabular}
 \end{quote2}
-
-As stated above, the two styles of declaration may appear together in the same block.
-Therefore, a programmer has the option of either continuing to use traditional C declarations or take advantage of the new style.
-Clearly, both styles need to be supported for some time due to existing C-style header-files, particularly for UNIX systems.
-In general, mixing declaration styles in a routine or even a translation unit is not recommended, as it makes a program more difficult to read.
-Therefore, it is suggested that an entire translation unit be written in one declaration style or the other.
 
 All type qualifiers, i.e., \lstinline@const@ and \lstinline@volatile@, are used in the normal way with the new declarations but appear left to right, e.g.:
@@ -510 +405 @@
 \begin{lstlisting}
 const * const int x;
-const * [ 10 ] const int y;
+const * [ 5 ] const int y;
 \end{lstlisting}
 &
 \begin{lstlisting}
 int const * const x;
-const int (* const y)[ 10 ]
+const int (* const y)[ 5 ]
 \end{lstlisting}
 &
 \begin{lstlisting}
 // const pointer to const integer
-// const pointer to array of 10 const integers
+// const pointer to array of 5 const integers
 \end{lstlisting}
 \end{tabular}
@@ -530 +425 @@
 \multicolumn{1}{c@{\hspace{30pt}}}{\textbf{\CFA}}       & \multicolumn{1}{c@{\hspace{20pt}}}{\textbf{C}}        \\
 \begin{lstlisting}
-extern [ 10 ] int x;
+extern [ 5 ] int x;
 static * const int y;
 \end{lstlisting}
 &
 \begin{lstlisting}
-int extern x[ 10 ];
+int extern x[ 5 ];
 const int static *y;
 \end{lstlisting}
 &
 \begin{lstlisting}
-// externally visible array of 10 integers
+// externally visible array of 5 integers
 // internally visible pointer to constant int
 \end{lstlisting}
 \end{tabular}
 \end{quote2}
+
+Unsupported are K\&R C declarations where the base type defaults to \lstinline@int@, if no type is specified\footnote{
+At least one type specifier shall be given in the declaration specifiers in each declaration, and in the specifier-qualifier list in each structure declaration and type name~\cite[\S~6.7.2(2)]{C11}},
+e.g.:
+\begin{lstlisting}
+x;                                              // int x
+*y;                                             // int *y
+f( p1, p2 );                    // int f( int p1, int p2 );
+f( p1, p2 ) {}                  // int f( int p1, int p2 ) {}
+\end{lstlisting}
+
+As stated above, the two styles of declaration may appear together in the same block.
+Therefore, a programmer has the option of either continuing to use traditional C declarations or take advantage of the new style.
+Clearly, both styles need to be supported for some time due to existing C-style header-files, particularly for UNIX systems.
 
 
@@ -555 +464 @@
 \begin{lstlisting}
 y = (* int)x;
-i = sizeof([ 10 ] * int);
+i = sizeof([ 5 ] * int);
 \end{lstlisting}
 &
 \begin{lstlisting}
 y = (int *)x;
-i = sizeof(int *[ 10 ]);
+i = sizeof(int *[ 5 ]);
 \end{lstlisting}
 \end{tabular}
@@ -571 +480 @@
 The point of the new syntax is to allow returning multiple values from a routine~\cite{CLU,Galletly96}, e.g.:
 \begin{lstlisting}
-[ int o1, int o2, char o3 ] f( int i1, char i2, char i3 ) {
-        @\emph{routine body}@
+®[ int o1, int o2, char o3 ]® f( int i1, char i2, char i3 ) {
+        §\emph{routine body}§
 }
 \end{lstlisting}
@@ -583 +492 @@
 Declaration qualifiers can only appear at the start of a routine definition, e.g.:
 \begin{lstlisting}
-extern [ int x ] g( int y ) {}
+extern [ int x ] g( int y ) {§\,§}
 \end{lstlisting}
 Lastly, if there are no output parameters or input parameters, the brackets and/or parentheses must still be specified;
 in both cases the type is assumed to be void as opposed to old style C defaults of int return type and unknown parameter types, respectively, as in:
 \begin{lstlisting}
-[ ] g();                                        // no input or output parameters
+[§\,§] g();                                             // no input or output parameters
 [ void ] g( void );                     // no input or output parameters
 \end{lstlisting}
@@ -600 +509 @@
 \CFA style declarations cannot be used to declare parameters for K\&R style routine definitions because of the following ambiguity:
 \begin{lstlisting}
-int (*f(x))[ 10 ] int x; {}
-\end{lstlisting}
-The string ``\lstinline@int (*f(x))[ 10 ]@'' declares a K\&R style routine of type returning a pointer to an array of 10 integers, while the string ``\lstinline@[ 10 ] int x@'' declares a \CFA style parameter x of type array of 10 integers.
+int (*f(x))[ 5 ] int x; {}
+\end{lstlisting}
+The string ``\lstinline@int (*f(x))[ 5 ]@'' declares a K\&R style routine of type returning a pointer to an array of 5 integers, while the string ``\lstinline@[ 5 ] int x@'' declares a \CFA style parameter x of type array of 5 integers.
 Since the strings overlap starting with the open bracket, \lstinline@[@, there is an ambiguous interpretation for the string.
 As well, \CFA-style declarations cannot be used to declare parameters for C-style routine-definitions because of the following ambiguity:
@@ -621 +530 @@
 \begin{lstlisting}
 #define ptoa( n, d ) int (*n)[ d ]
-int f( ptoa(p,10) ) ...         // expands to int f( int (*p)[ 10 ] )
-[ int ] f( ptoa(p,10) ) ...     // expands to [ int ] f( int (*p)[ 10 ] )
+int f( ptoa(p,5) ) ...          // expands to int f( int (*p)[ 5 ] )
+[ int ] f( ptoa(p,5) ) ...      // expands to [ int ] f( int (*p)[ 5 ] )
 \end{lstlisting}
 Again, programmers are highly encouraged to use one declaration form or the other, rather than mixing the forms.
@@ -639 +548 @@
 Because the value in the return variable is automatically returned when a \CFA routine terminates, the \lstinline@return@ statement \emph{does not} contain an expression, as in:
 \begin{lstlisting}
-[ int x ] f() {
+®[ int x ]® f() {
         ... x = 0; ... x = y; ...
-        return; // implicitly return x
+        ®return;® // implicitly return x
 }
 \end{lstlisting}
@@ -697 +606 @@
 for example, the following is incorrect:
 \begin{lstlisting}
-* [ int x ] f () fp;            // routine name ``f'' is not allowed
+* [ int x ] f () fp;            // routine name "f" is not allowed
 \end{lstlisting}
 
@@ -703 +612 @@
 \section{Named and Default Arguments}
 
-Named and default arguments~\cite{Hardgrave76}.\footnote{
+Named and default arguments~\cite{Hardgrave76}\footnote{
 Francez~\cite{Francez77} proposed a further extension to the named-parameter passing style, which specifies what type of communication (by value, by reference, by name) the argument is passed to the routine.}
 are two mechanisms to simplify routine call.
@@ -864 +773 @@
 \subsection{Type Nesting}
 
-C allows \Index{type nesting}, but the nested types are hoisted\index{type!hoisting} (refactored) into the enclosing scope.
+\CFA allows \Index{type nesting}, and type qualification of the nested types, where as C hoists\index{type hoisting} (refactors) nested types into the enclosing scope and has no type qualification.
 \begin{quote2}
 \begin{tabular}{@{}l@{\hspace{30pt}}l|l@{}}
@@ -919 +828 @@
 
 int fred() {
-        s.t.c = S.R;
-        struct S.T t = { S.R, 1, 2 };
-        enum S.C c;
-        union S.T.U u;
+        s.t.c = ®S.®R;  // type qualification
+        struct ®S.®T t = { ®S.®R, 1, 2 };
+        enum ®S.®C c;
+        union ®S.T.®U u;
 }
 \end{lstlisting}
 \end{tabular}
 \end{quote2}
-
-\CFA is C \emph{incompatible} on this issue, and provides semantics similar to \CC.
-Nested types are not hoisted and can be referenced using the field selection operator ``\lstinline@.@'', unlike the \CC scope-resolution operator ``\lstinline@::@''.
-Given that nested types in C are equivalent to not using them, i.e., they are essentially useless, it is unlikely there are any realistic usages that break because of this incompatibility.
+In the left example in C, types \lstinline@C@, \lstinline@U@ and \lstinline@T@ are implicitly hoisted outside of type \lstinline@S@ into the containing block scope.
+In the right example in \CFA, the types are not hoisted and accessed using the field-selection operator ``\lstinline@.@'' for type qualification, as does Java, rather than the \CC type-selection operator ``\lstinline@::@''.
 
 
@@ -943 +850 @@
 which can be used to sort in ascending and descending order by locally redefining the less-than operator into greater-than.
 \begin{lstlisting}
-const unsigned int size = 10;
-int a[size];
-
-qsort( a, size );               // ascending order using built in ?<?
-{                                               // descending order by local redefinition
-        int ?<?( int a, int b ) { return a > b; } // nested routine
-        qsort( a, size );
-}
-\end{lstlisting}
-
-
-\section{Incompatible}
-
-The following incompatibles exist between C and \CFA, and are similar to Annex C for \CC~\cite{ANSI14:C++}.
-
-\begin{enumerate}
-\item
-Change type of character literal \lstinline@int@ to \lstinline@char@.
-This change allows overloading differentiation argument type matching, e.g.:
-\begin{lstlisting}
-int function( int i );
-int function( char c );
-function( 'x' );
-\end{lstlisting}
-It is preferable that this call match the second version of function rather than the first. \\
-Effect on original feature: Change to semantics of well-defined feature. ISO C programs which depend on
-\begin{lstlisting}
-sizeof('x') == sizeof(int)
-\end{lstlisting}
-will not work the same as C++ programs. \\
-Difficulty of converting: Simple. \\
-How widely used: Programs which depend upon sizeof('x') are probably rare.
-
-\item
-Change: String literals made \lstinline@const@ \\
-The type of a string literal is changed from \lstinline@array of char@ to \lstinline@array of const char@.
-The type of a wide string literal is changed from \lstinline@array of wchar_t@ to \lstinline@array of const wchar_t@. \\
-Rationale: This avoids calling an inappropriate overloaded function, which might expect to be able to modify its argument.
-Effect on original feature: Change to semantics of well-defined feature. \\
-Difficulty of converting: Simple syntactic transformation, because string literals can be converted to \lstinline@char*;@ (4.2).
-The most common cases are handled by a new but deprecated standard conversion:
-\begin{lstlisting}
-char* p = "abc"; // valid in C, deprecated in C++
-char* q = expr ? "abc" : "de"; // valid in C, invalid in C++
-\end{lstlisting}
-How widely used: Programs that have a legitimate reason to treat string literals as pointers to potentially modifiable memory are probably rare.
-
-\item
-Change: C++ does not have \emph{tentative definitions} as in C.
-E.g., at file scope,
-\begin{lstlisting}
-int i;
-int i;
-\end{lstlisting}
-is valid in C, invalid in C++.
-This makes it impossible to define mutually referential file-local static
-objects, if initializers are restricted to the syntactic forms of C. For example,
-\begin{lstlisting}
-struct X { int i; struct X *next; };
-static struct X a;
-static struct X b = { 0, &a };
-static struct X a = { 1, &b };
-\end{lstlisting}
-Rationale: This avoids having different initialization rules for builtin types and userdefined types.
-Effect on original feature: Deletion of semantically welldefined feature. \\
-Difficulty of converting: Semantic transformation.
-In C++, the initializer for one of a set of mutuallyreferential filelocal static objects must invoke a function call to achieve the initialization.
-How widely used: Seldom.
-
-\item
-Change: A struct is a scope in C++, not in C
-Rationale: Class scope is crucial to C++, and a struct is a class.
-Effect on original feature: Change to semantics of well-defined feature.
-Difficulty of converting: Semantic transformation.
-How widely used: C programs use struct extremely frequently, but the change is only noticeable when
-struct, enumeration, or enumerator names are referred to outside the struct. The latter is probably
-rare.
-
-\item
-Change: In C++, the name of a nested class is local to its enclosing class.
-In C the name of the nested class belongs to the same scope as the name of the outermost enclosing class
-Example:
-\begin{lstlisting}
-struct X {
-struct Y { /* ... */ } y;
-};
-struct Y yy; // valid C, invalid C++
-\end{lstlisting}
-Rationale: C++ classes have member functions which require that classes establish scopes. The C rule
-would leave classes as an incomplete scope mechanism which would prevent C++ programmers from maintaining
-locality within a class. A coherent set of scope rules for C++ based on the C rule would be very
-complicated and C++ programmers would be unable to predict reliably the meanings of nontrivial examples
-involving nested or local functions.
-Effect on original feature: Change of semantics of welldefined
-feature.
-Difficulty of converting: Semantic transformation. To make the struct type name visible in the scope of
-the enclosing struct, the struct tag could be declared in the scope of the enclosing struct, before the enclosing
-struct is defined. Example:
-\begin{lstlisting}
-struct Y; // struct Y and struct X are at the same scope
-struct X {
-struct Y { /* ... */ } y;
-};
-\end{lstlisting}
-All the definitions of C struct types enclosed in other struct definitions and accessed outside the scope of
-the enclosing struct could be exported to the scope of the enclosing struct. Note: this is a consequence of
-the difference in scope rules, which is documented in 3.3.
-How widely used: Seldom.
-\end{enumerate}
+const unsigned int size = 5;
+int ia[size];
+...                                             // assign values to array ia
+qsort( ia, size );              // sort ascending order using builtin ?<?
+{
+        ®int ?<?( int x, int y ) { return x > y; }® // nested routine
+        qsort( ia, size );      // sort descending order by local redefinition
+}
+\end{lstlisting}
+
+Nested routines are not first-class, meaning a nested routine cannot be returned if it has references to variables in its enclosing blocks;
+the only exception is references to the external block of the translation unit, as these variables persist for the duration of the program.
+The following program in undefined in \CFA (and \lstinline@gcc@\index{gcc})
+\begin{lstlisting}
+[* [int]( int )] foo() {                // int (*foo())( int )
+        int ®i® = 7;
+        int bar( int p ) {
+                ®i® += 1;                                       // dependent on local variable
+                sout | ®i® | endl;
+        }
+        return bar;                                     // undefined because of local dependence
+}
+int main() {
+        * [int](int) fp = foo();        // int (*fp)(int)
+    sout | fp( 3 ) | endl;
+}
+\end{lstlisting}
+because 
+
+Currently, there are no \Index{lambda} expressions, i.e., unnamed routines because routine names are very important to properly select the correct routine.
 
 
@@ -1061 +889 @@
 The general syntax of a tuple is:
 \begin{lstlisting}
-[ $\emph{exprlist}$ ]
+[ §\emph{exprlist}§ ]
 \end{lstlisting}
 where \lstinline@$\emph{exprlist}$@ is a list of one or more expressions separated by commas.
@@ -1081 +909 @@
 The general syntax of a tuple type is:
 \begin{lstlisting}
-[ @\emph{typelist}@ ]
+[ §\emph{typelist}§ ]
 \end{lstlisting}
 where \lstinline@$\emph{typelist}$@ is a list of one or more legal \CFA or C type specifications separated by commas, which may include other tuple type specifications.
@@ -1089 +917 @@
 [ double, double, double ]
 [ * int, int * ]                // mix of CFA and ANSI
-[ * [ 10 ] int, * * char, * [ [ int, int ] ] (int, int) ]
+[ * [ 5 ] int, * * char, * [ [ int, int ] ] (int, int) ]
 \end{lstlisting}
 Like tuples, tuple types may be nested, such as \lstinline@[ [ int, int ], int ]@, which is a 2-element tuple type whose first element is itself a tuple type.
@@ -1185 +1013 @@
 First the right-hand tuple is flattened and then the values are assigned individually.
 Flattening is also performed on tuple types.
-For example, the type \lstinline@[ int, [ int, int ], int ]@ can be coerced, using flattening, into the type lstinline@[ int, int, int, int ]@.
+For example, the type \lstinline@[ int, [ int, int ], int ]@ can be coerced, using flattening, into the type \lstinline@[ int, int, int, int ]@.
 
 A \newterm{structuring coercion} is the opposite of flattening;
@@ -1211 +1039 @@
 Mass assignment has the following form:
 \begin{lstlisting}
-[ @\emph{lvalue}@, ..., @\emph{lvalue}@ ] = @\emph{expr}@;
-\end{lstlisting}
-The left-hand side is a tuple of \lstinline@$\emph{lvalues}$@, which is a list of expressions each yielding an address, i.e., any data object that can appear on the left-hand side of a conventional assignment statement.
+[ §\emph{lvalue}§, ..., §\emph{lvalue}§ ] = §\emph{expr}§;
+\end{lstlisting}
+The left-hand side is a tuple of \emph{lvalues}, which is a list of expressions each yielding an address, i.e., any data object that can appear on the left-hand side of a conventional assignment statement.
 \lstinline@$\emph{expr}$@ is any standard arithmetic expression.
 Clearly, the types of the entities being assigned must be type compatible with the value of the expression.
@@ -1250 +1078 @@
 Multiple assignment has the following form:
 \begin{lstlisting}
-[ @\emph{lvalue}@, . . ., @\emph{lvalue}@ ] = [ @\emph{expr}@, . . ., @\emph{expr}@ ];
-\end{lstlisting}
-The left-hand side is a tuple of \lstinline@$\emph{lvalues}$@, and the right-hand side is a tuple of \lstinline@$\emph{expr}$@s.
-Each \lstinline@$\emph{expr}$@ appearing on the righthand side of a multiple assignment statement is assigned to the corresponding \lstinline@$\emph{lvalues}$@ on the left-hand side of the statement using parallel semantics for each assignment.
+[ §\emph{lvalue}§, . . ., §\emph{lvalue}§ ] = [ §\emph{expr}§, . . ., §\emph{expr}§ ];
+\end{lstlisting}
+The left-hand side is a tuple of \emph{lvalues}, and the right-hand side is a tuple of \emph{expr}s.
+Each \emph{expr} appearing on the righthand side of a multiple assignment statement is assigned to the corresponding \emph{lvalues} on the left-hand side of the statement using parallel semantics for each assignment.
 An example of multiple assignment is:
 \begin{lstlisting}
@@ -1290 +1118 @@
 Cascade assignment has the following form:
 \begin{lstlisting}
-@\emph{tuple}@ = @\emph{tuple}@ = ... = @\emph{tuple}@;
+§\emph{tuple}§ = §\emph{tuple}§ = ... = §\emph{tuple}§;
 \end{lstlisting}
 and it has the same parallel semantics as for mass and multiple assignment.
@@ -1308 +1136 @@
 Its general form is:
 \begin{lstlisting}
-@\emph{expr}@ . [ @\emph{fieldlist}@ ]
-@\emph{expr}@ -> [ @\emph{fieldlist}@ ]
-\end{lstlisting}
-\lstinline@$\emph{expr}$@ is any expression yielding a value of type record, e.g., \lstinline@struct@, \lstinline@union@.
-Each element of \lstinline@$\emph{ fieldlist}$@ is an element of the record specified by \lstinline@$\emph{expr}$@.
+§\emph{expr}§ . [ §\emph{fieldlist}§ ]
+§\emph{expr}§ -> [ §\emph{fieldlist}§ ]
+\end{lstlisting}
+\emph{expr} is any expression yielding a value of type record, e.g., \lstinline@struct@, \lstinline@union@.
+Each element of \emph{ fieldlist} is an element of the record specified by \emph{expr}.
 A record-field tuple may be used anywhere a tuple can be used. An example of the use of a record-field tuple is
 the following:
@@ -1352 +1180 @@
 \multicolumn{1}{c@{\hspace{30pt}}}{\textbf{\CFA}}       & \multicolumn{1}{c}{\textbf{C}}        \\
 \begin{lstlisting}
-L1: for ( ... ) {
-        L2: for ( ... ) {
-                L3: for ( ... ) {
-                        ... break L1; ...
-                        ... break L2; ...
-                        ... break L3; // or break
+®L1:® for ( ... ) {
+        ®L2:® for ( ... ) {
+                ®L3:® for ( ... ) {
+                        ... break ®L1®; ...
+                        ... break ®L2®; ...
+                        ... break ®L3®; // or break
                 }
         }
@@ -1382 +1210 @@
 \multicolumn{1}{c@{\hspace{30pt}}}{\textbf{\CFA}}       & \multicolumn{1}{c}{\textbf{C}}        \\
 \begin{lstlisting}
-L1: for ( ... ) {
-        L2: for ( ... ) {
-                L3: for ( ... ) {
-                        ... continue L1; ...
-                        ... continue L2; ...
-                        ... continue L3; ...
+®L1®: for ( ... ) {
+        ®L2®: for ( ... ) {
+                ®L3®: for ( ... ) {
+                        ... continue ®L1®; ...
+                        ... continue ®L2®; ...
+                        ... continue ®L3®; ...
 
                 }
@@ -1623 +1451 @@
 \begin{lstlisting}
 switch ( i ) {
-  case 1, 3, 5:
+  ®case 1, 3, 5®:
         ...
-  case 2, 4, 6:
+  ®case 2, 4, 6®:
         ...
 }
@@ -1634 +1462 @@
   case 1: case 3 : case 5:
         ...
-  case 2: case 4 : case 6: /* even values */
+  case 2: case 4 : case 6:
         ...
 }
@@ -1655 +1483 @@
 \begin{lstlisting}
 switch ( i ) {
-  case 1~5
+  ®case 1~5:®
         ...
-  case 10~15
+  ®case 10~15:®
         ...
 }
@@ -1672 +1500 @@
 &
 \begin{lstlisting}
+
 // 1, 2, 3, 4, 5
 
@@ -2168 +1997 @@
 
 
-\section{Generics }
+\section{Auto Type-Inferencing}
+
+Auto type-inferencing occurs in a declaration where a variable's type is inferred from its initialization expression type.
+\begin{quote2}
+\begin{tabular}{@{}l@{\hspace{30pt}}ll@{}}
+\multicolumn{1}{c@{\hspace{30pt}}}{\textbf{\CC}}        & \multicolumn{1}{c}{\lstinline@gcc@}\index{gcc} \\
+\begin{lstlisting}
+
+auto j = 3.0 * 4;
+int i;
+auto k = i;
+\end{lstlisting}
+&
+\begin{lstlisting}
+#define expr 3.0 * i
+typeof(expr) j = expr;
+int i;
+typeof(i) k = i;
+\end{lstlisting}
+&
+\begin{lstlisting}
+
+// use type of initialization expression
+
+// use type of primary variable
+\end{lstlisting}
+\end{tabular}
+\end{quote2}
+The two important capabilities are:
+\begin{itemize}
+\item
+preventing having to determine or write out long generic types,
+\item
+ensure secondary variables, related to a primary variable, always have the same type.
+\end{itemize}
+
+In \CFA, \lstinline@typedef@ provides a mechanism to alias long type names with short ones, both globally and locally, but not eliminate the use of the short name.
+\lstinline@gcc@ provides \lstinline@typeof@ to declare a secondary variable from a primary variable.
+\CFA also relies heavily on the specification of the left-hand side of assignment for type inferencing, so in many cases it is crucial to specify the type of the left-hand side to select the correct type of the right-hand expression.
+Only for overloaded routines with the same return type is variable type-inferencing possible.
+Finally, \lstinline@auto@ presents the programming problem of tracking down a type when the type is actually needed.
+For example, given
+\begin{lstlisting}
+auto j = ®...®
+\end{lstlisting}
+and the need to write a routine to compute using \lstinline@j@
+\begin{lstlisting}
+void rtn( ®...® parm );
+rtn( j );
+\end{lstlisting}
+A programmer must work backwards to determine the type of \lstinline@j@'s initialization expression, reconstructing the possibly long generic type-name.
+In this situation, having the type name or a short alias is very useful.
+
+There is also the conundrum in type inferencing of when to \emph{\Index{brand}} a type.
+That is, when is the type of the variable more important than the type of its initialization expression.
+For example, if a change is made in an initialization expression, it can cause hundreds or thousands of cascading type changes and/or errors.
+At some point, a programmer wants the type of the variable to remain constant and the expression to be in error when it changes.
+
+Given \lstinline@typedef@ and \lstinline@typeof@ in \CFA, and the strong need to use the type of left-hand side in inferencing, auto type-inferencing is not supported at this time.
+Should a significant need arise, this feature can be revisited.
+
+
+\section{Generics}
 
 \CFA supports parametric polymorphism to allow users to define generic functions and types.
@@ -2368 +2259 @@
 
         try {
-        throw 13;
+                throw 13;
         }
         catch(int e) {
-        printf(.caught an exception: %d\n., e);
+                printf(.caught an exception: %d\n., e);
         }
 \end{lstlisting}
@@ -2457 +2348 @@
 
 
-\section{I/O Library}
-\label{s:IOLibrary}
-
-The goal for \CFA I/O is to make I/O as simple as possible for the general case, while fully supporting polmorphism and user defined types in a consistent way.
-The general case is printing out a sequence of variables separated by whitespace.
-\begin{lstlisting}
-int x = 0, y = 1, z = 2;
-sout | x | y | z | endl;
-
-cout << x << " " << y << " " << z << endl;
-\end{lstlisting}
-The \CC form takes almost twice as many characters.
-
-The logical-or operator is used because it is the lowest priority overloadable operator, other than assignment.
-Therefore, most output expressions do not require parenthesis.
-\begin{lstlisting}
-int x = 0, y = 1, z = 2;
-sout | x * 3 | y + 1 | z << 2 | x == y | (x | y) | (x || y) | (x > z ? 1 : 2) | endl;
-
-cout << x * 3 << y + 1 << (z << 2) << (x == y) << (x | y) << (x || y) << (x > z ? 1 : 2) << endl;
-\end{lstlisting}
-
-Finally, the logical-or operator has a link with the Shell pipe-operator for moving data, although data flows in the opposite direction.
-
-\begin{figure}
-\begin{lstlisting}[mathescape=off]
-#include <fstream>
-
-int main() {
-        char c;
-        short int si;
-        unsigned short int usi;
-        int i;
-        unsigned int ui;
-        long int li;
-        unsigned long int uli;
-        long long int lli;
-        unsigned long long int ulli;
-        float f;
-        double d;
-        long double ld;
-        float _Complex fc;
-        double _Complex dc;
-        long double _Complex ldc;
-        char s1[10], s2[10];
-
-        ifstream in;
-        open( &in, "read.data", "r" );
-
-        &in | &c
-                | &si | &usi | &i | &ui | &li | &uli | &lli | &ulli
-                | &f | &d | &ld
-                | &fc | &dc | &ldc
-                | str( s1 ) | str( s2, 10 );
-
-        sout | c | ' ' | endl
-                 | si | usi | i | ui | li | uli | lli | ulli | endl
-                 | f | d | ld | endl
-                 | f | "" | d | "" | ld | endl;
-
-        sepSet( sout, ", $" );
-        sout | fc | dc | ldc | endl
-                 | sepOn | s1 | sepOff | s2 | endl
-                 | s1 | "" | s2 | endl;
-}
-
-$ cat read.data 
-A 1 2 3 4 5 6 7 8 1.1 1.2 1.3 1.1+2.3 1.1-2.3 1.1-2.3 abc xyz
-$ a.out
-A 
-1 2 3 4 5 6 7 8
-1.1 1.2 1.3
-1.11.21.3
-1.1+2.3i, $1.1-2.3i, $1.1-2.3i
-, $abcxyz
-abcxyz
-\end{lstlisting}
-\end{figure}
-
-
-\section{Standard Library}
-\label{s:StandardLibrary}
-
-The goal of the \CFA standard-library is to wrap many of the existing C library-routines that are explicitly polymorphic into implicitly polymorphic versions.
-
-
-\subsection{malloc}
-
-\begin{lstlisting}
-forall( otype T ) T * malloc( void );
-forall( otype T ) T * malloc( char fill );
-forall( otype T ) T * malloc( T * ptr, size_t size );
-forall( otype T ) T * malloc( T * ptr, size_t size, unsigned char fill );
-forall( otype T ) T * calloc( size_t size );
-forall( otype T ) T * realloc( T * ptr, size_t size );
-forall( otype T ) T * realloc( T * ptr, size_t size, unsigned char fill );
-
-forall( otype T ) T * aligned_alloc( size_t alignment );
-forall( otype T ) T * memalign( size_t alignment );             // deprecated
-forall( otype T ) int posix_memalign( T ** ptr, size_t alignment );
-
-forall( otype T ) T * memset( T * ptr, unsigned char fill ); // use default value '\0' for fill
-forall( otype T ) T * memset( T * ptr );                                // remove when default value available
-\end{lstlisting}
-
-
-\subsection{ato/strto}
-
-\begin{lstlisting}
-int ato( const char * ptr );
-unsigned int ato( const char * ptr );
-long int ato( const char * ptr );
-unsigned long int ato( const char * ptr );
-long long int ato( const char * ptr );
-unsigned long long int ato( const char * ptr );
-float ato( const char * ptr );
-double ato( const char * ptr );
-long double ato( const char * ptr );
-float _Complex ato( const char * ptr );
-double _Complex ato( const char * ptr );
-long double _Complex ato( const char * ptr );
-
-int strto( const char * sptr, char ** eptr, int base );
-unsigned int strto( const char * sptr, char ** eptr, int base );
-long int strto( const char * sptr, char ** eptr, int base );
-unsigned long int strto( const char * sptr, char ** eptr, int base );
-long long int strto( const char * sptr, char ** eptr, int base );
-unsigned long long int strto( const char * sptr, char ** eptr, int base );
-float strto( const char * sptr, char ** eptr );
-double strto( const char * sptr, char ** eptr );
-long double strto( const char * sptr, char ** eptr );
-float _Complex strto( const char * sptr, char ** eptr );
-double _Complex strto( const char * sptr, char ** eptr );
-long double _Complex strto( const char * sptr, char ** eptr );
-\end{lstlisting}
-
-
-\subsection{bsearch/qsort}
-
-\begin{lstlisting}
-forall( otype T | { int ?<?( T, T ); } )
-T * bsearch( const T key, const T * arr, size_t dimension );
-
-forall( otype T | { int ?<?( T, T ); } )
-void qsort( const T * arr, size_t dimension );
-\end{lstlisting}
-
-
-\subsection{abs}
-
-\begin{lstlisting}
-char abs( char );
-extern "C" {
-int abs( int );         // use default C routine for int
-} // extern
-long int abs( long int );
-long long int abs( long long int );
-float abs( float );
-double abs( double );
-long double abs( long double );
-float _Complex abs( float _Complex );
-double _Complex abs( double _Complex );
-long double _Complex abs( long double _Complex );
-\end{lstlisting}
-
-
-\subsection{random}
-
-\begin{lstlisting}
-void randseed( long int s );
-char random();
-int random();
-unsigned int random();
-long int random();
-unsigned long int random();
-float random();
-double random();
-float _Complex random();
-double _Complex random();
-long double _Complex random();
-\end{lstlisting}
-
-
-\subsection{min/max/swap}
-
-\begin{lstlisting}
-forall( otype T | { int ?<?( T, T ); } )
-T min( const T t1, const T t2 );
-
-forall( otype T | { int ?>?( T, T ); } )
-T max( const T t1, const T t2 );
-
-forall( otype T )
-void swap( T * t1, T * t2 );
-\end{lstlisting}
+\section{Syntactic Anomalies}
+
+The number 0 and 1 are treated specially in \CFA, and can be redefined as variables.
+One syntactic anomaly is when a field in an structure is names 0 or 1:
+\begin{lstlisting}
+struct S {
+        int 0, 1;
+} s;
+\end{lstlisting}
+The problem occurs in accesing these fields using the selection operation ``\lstinline@.@'':
+\begin{lstlisting}
+s.0 = 0;        // ambiguity with floating constant .0
+s.1 = 1;        // ambiguity with floating constant .1
+\end{lstlisting}
+To make this work, a space is required after the field selection:
+\begin{lstlisting}
+®s.§\textvisiblespace§0® = 0;
+®s.§\textvisiblespace§1® = 1;
+\end{lstlisting}
+While this sytact is awkward, it is unlikely many programers will name fields of a structure 0 or 1.
+Like the \CC lexical problem with closing template-syntax, e.g, \lstinline@Foo<Bar<int®>>®@, this issue can be solved with a more powerful lexer/parser.
+
+There are several ambiguous cases with operator identifiers, e.g., \lstinline@int *?*?()@, where the string \lstinline@*?*?@ can be lexed as \lstinline@*@/\lstinline@?*?@ or \lstinline@*?@/\lstinline@*?@.
+Since it is common practise to put a unary operator juxtaposed to an identifier, e.g., \lstinline@*i@, users will be annoyed if they cannot do this with respect to operator identifiers.
+Even with this special hack, there are 5 general cases that cannot be handled.
+The first case is for the function-call identifier \lstinline@?()@:
+\begin{lstlisting}
+int *§\textvisiblespace§?()();  // declaration: space required after '*'
+*§\textvisiblespace§?()();              // expression: space required after '*'
+\end{lstlisting}
+Without the space, the string \lstinline@*?()@ is ambiguous without N character look ahead;
+it requires scanning ahead to determine if there is a \lstinline@'('@, which is the start of an argument/parameter list.
+
+The 4 remaining cases occur in expressions:
+\begin{lstlisting}
+i++§\textvisiblespace§?i:0;             // space required before '?'
+i--§\textvisiblespace§?i:0;             // space required before '?'
+i§\textvisiblespace§?++i:0;             // space required after '?'
+i§\textvisiblespace§?--i:0;             // space required after '?'
+\end{lstlisting}
+In the first two cases, the string \lstinline@i++?@ is ambiguous, where this string can be lexed as \lstinline@i@ / \lstinline@++?@ or \lstinline@i++@ / \lstinline@?@;
+it requires scanning ahead to determine if there is a \lstinline@'('@, which is the start of an argument list.
+In the second two cases, the string \lstinline@?++x@ is ambiguous, where this string can be lexed as \lstinline@?++@ / \lstinline@x@ or \lstinline@?@ / y\lstinline@++x@;
+it requires scanning ahead to determine if there is a \lstinline@'('@, which is the start of an argument list.
 
 
@@ -2676 +2416 @@
 
 task creates a type with implicit locking, separate stack, and a thread
+
 
 \subsection{Monitors}
@@ -3576 +3317 @@
 
 
-\subsection{Comparing Key Features of \CFA}
+\subsection[Comparing Key Features of CFA]{Comparing Key Features of \CFA}
 
 
@@ -3775 +3516 @@
 \multicolumn{1}{c|}{\textbf{\CFA/\CC}} & \multicolumn{1}{c|}{\textbf{Go}} & \multicolumn{1}{c}{\textbf{Rust}}   \\
 \hline
-\begin{lstlisting}
+\begin{lstlisting}[boxpos=t]
 extern "C" {
 #include <sys/types.h>
@@ -3782 +3523 @@
 }
 size_t fileSize( const char *path ) {
-        stat s;
+        struct stat s;
         stat(path, &s);
         return s.st_size;
@@ -3788 +3529 @@
 \end{lstlisting}
 &
-\begin{lstlisting}
+\begin{lstlisting}[boxpos=t]
 /*
 #cgo
@@ -3807 +3548 @@
 \end{lstlisting}
 &
-\begin{lstlisting}
+\begin{lstlisting}[boxpos=t]
 use libc::{c_int, size_t};
-
-// The following declarations are
 // translated from sys/stat.h
 #[repr(C)]
@@ -3818 +3557 @@
         ...
 }
-
 #[link(name = "libc")]
 extern {
@@ -3824 +3562 @@
         buf: *mut stat_t) -> c_int;
 }
-
 fn fileSize(path: *const u8) -> size_t
 {
         unsafe {
-        let mut buf: stat_t = uninit();
-        stat(path, &mut buf);
-        buf.st_size
+                let mut buf: stat_t = uninit();
+                stat(path, &mut buf);
+                buf.st_size
         }
 }
@@ -3953 +3690 @@
 
 
-\subsubsection{Modules/Packages}
+\begin{comment}
+\subsubsection{Modules / Packages}
 
 \begin{lstlisting}
@@ -4032 +3770 @@
 }
 \end{lstlisting}
+\end{comment}
+
 
 \subsubsection{Parallel Tasks}
@@ -4187 +3927 @@
 \end{flushleft}
 
+\lstset{basicstyle=\sf\relsize{-1}}
+
+
 \subsection{Summary of Language Comparison}
 
 
-\subsubsection{\CC}
+\subsubsection[C++]{\CC}
 
 \CC is a general-purpose programming language.
@@ -4255 +3998 @@
 
 
+\appendix
+
+
+\section{Incompatible}
+
+The following incompatibles exist between C and \CFA, and are similar to Annex C for \CC~\cite{ANSI14:C++}.
+
+\begin{enumerate}
+\item
+Change type of character literal \lstinline@int@ to \lstinline@char@.
+This change allows overloading differentiation argument type matching, e.g.:
+\begin{lstlisting}
+int function( int i );
+int function( char c );
+function( 'x' );
+\end{lstlisting}
+It is preferable that this call match the second version of function rather than the first. \\
+Effect on original feature: Change to semantics of well-defined feature. ISO C programs which depend on
+\begin{lstlisting}
+sizeof('x') == sizeof(int)
+\end{lstlisting}
+will not work the same as C++ programs. \\
+Difficulty of converting: Simple. \\
+How widely used: Programs which depend upon sizeof('x') are probably rare.
+
+\item
+Change: String literals made \lstinline@const@ \\
+The type of a string literal is changed from \lstinline@array of char@ to \lstinline@array of const char@.
+The type of a wide string literal is changed from \lstinline@array of wchar_t@ to \lstinline@array of const wchar_t@. \\
+Rationale: This avoids calling an inappropriate overloaded function, which might expect to be able to modify its argument.
+Effect on original feature: Change to semantics of well-defined feature. \\
+Difficulty of converting: Simple syntactic transformation, because string literals can be converted to \lstinline@char*;@ (4.2).
+The most common cases are handled by a new but deprecated standard conversion:
+\begin{lstlisting}
+char* p = "abc"; // valid in C, deprecated in C++
+char* q = expr ? "abc" : "de"; // valid in C, invalid in C++
+\end{lstlisting}
+How widely used: Programs that have a legitimate reason to treat string literals as pointers to potentially modifiable memory are probably rare.
+
+\item
+Change: C++ does not have \emph{tentative definitions} as in C.
+E.g., at file scope,
+\begin{lstlisting}
+int i;
+int i;
+\end{lstlisting}
+is valid in C, invalid in C++.
+This makes it impossible to define mutually referential file-local static
+objects, if initializers are restricted to the syntactic forms of C. For example,
+\begin{lstlisting}
+struct X { int i; struct X *next; };
+static struct X a;
+static struct X b = { 0, &a };
+static struct X a = { 1, &b };
+\end{lstlisting}
+Rationale: This avoids having different initialization rules for builtin types and userdefined types.
+Effect on original feature: Deletion of semantically welldefined feature. \\
+Difficulty of converting: Semantic transformation.
+In C++, the initializer for one of a set of mutuallyreferential filelocal static objects must invoke a function call to achieve the initialization.
+How widely used: Seldom.
+
+\item
+Change: A struct is a scope in C++, not in C \\
+Rationale: Class scope is crucial to C++, and a struct is a class. \\
+Effect on original feature: Change to semantics of well-defined feature. \\
+Difficulty of converting: Semantic transformation. \\
+How widely used: C programs use struct extremely frequently, but the change is only noticeable when struct, enumeration, or enumerator names are referred to outside the struct.
+The latter is probably rare.
+
+\CFA is C \emph{incompatible} on this issue, and provides semantics similar to \CC.
+Nested types are not hoisted and can be referenced using the field selection operator ``\lstinline@.@'', unlike the \CC scope-resolution operator ``\lstinline@::@''.
+Given that nested types in C are equivalent to not using them, i.e., they are essentially useless, it is unlikely there are any realistic usages that break because of this incompatibility.
+
+\item
+Change: In C++, the name of a nested class is local to its enclosing class.
+In C the name of the nested class belongs to the same scope as the name of the outermost enclosing class
+Example:
+\begin{lstlisting}
+struct X {
+struct Y { /* ... */ } y;
+};
+struct Y yy; // valid C, invalid C++
+\end{lstlisting}
+Rationale: C++ classes have member functions which require that classes establish scopes.
+The C rule would leave classes as an incomplete scope mechanism which would prevent C++ programmers from maintaining locality within a class. A coherent set of scope rules for C++ based on the C rule would be very complicated and C++ programmers would be unable to predict reliably the meanings of nontrivial examples involving nested or local functions.
+Effect on original feature: Change of semantics of welldefined feature.
+Difficulty of converting: Semantic transformation. To make the struct type name visible in the scope of the enclosing struct, the struct tag could be declared in the scope of the enclosing struct, before the enclosing struct is defined. Example:
+\begin{lstlisting}
+struct Y; // struct Y and struct X are at the same scope
+struct X {
+struct Y { /* ... */ } y;
+};
+\end{lstlisting}
+All the definitions of C struct types enclosed in other struct definitions and accessed outside the scope of the enclosing struct could be exported to the scope of the enclosing struct.
+Note: this is a consequence of the difference in scope rules, which is documented in 3.3.
+How widely used: Seldom.
+\end{enumerate}
+
+
+\section{I/O Library}
+\label{s:IOLibrary}
+\index{input/output library}
+
+The goal for \CFA I/O is to make I/O as simple as possible for the general case, while fully supporting polmorphism and user defined types in a consistent way.
+The general case is printing out a sequence of variables separated by whitespace.
+\begin{quote2}
+\begin{tabular}{@{}l@{\hspace{30pt}}l@{}}
+\multicolumn{1}{c@{\hspace{30pt}}}{\textbf{\CFA}}       & \multicolumn{1}{c}{\textbf{\CC}}      \\
+\begin{lstlisting}
+int x = 0, y = 1, z = 2;
+®sout® ®|® x ®|® y ®|® z ®| endl®;
+\end{lstlisting}
+&
+\begin{lstlisting}
+
+cout << x << " " << y << " " << z << endl;
+\end{lstlisting}
+\end{tabular}
+\end{quote2}
+The \CFA form is half as many characters, and is similar to \Index{Python} I/O with respect to implicit separators.
+
+The logical-or operator is used because it is the lowest-priority overloadable operator, other than assignment.
+Therefore, fewer output expressions require parenthesis.
+\begin{quote2}
+\begin{tabular}{@{}ll@{}}
+\textbf{\CFA:}
+&
+\begin{lstlisting}
+sout | x * 3 | y + 1 | z << 2 | x == y | (x | y) | (x || y) | (x > z ? 1 : 2) | endl;
+\end{lstlisting}
+\\
+\textbf{\CC:}
+&
+\begin{lstlisting}
+cout << x * 3 << y + 1 << (z << 2) << (x == y) << (x | y) << (x || y) << (x > z ? 1 : 2) << endl;
+\end{lstlisting}
+\end{tabular}
+\end{quote2}
+Finally, the logical-or operator has a link with the Shell pipe-operator for moving data, although data flows in the opposite direction.
+
+The implicit seperator\index{I/O separator} character (space/blank) is a separator not a terminator.
+The rules for implicitly adding the separator are:
+\begin{enumerate}
+\item
+A seperator does not appear at the start or end of a line.
+\begin{lstlisting}[belowskip=0pt]
+sout | 1 | 2 | 3 | endl;
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+1 2 3
+\end{lstlisting}
+\item
+A seperator does not appear before or after a character literal or variable.
+\begin{lstlisting}
+sout | '1' | '2' | '3' | endl;
+123
+\end{lstlisting}
+\item
+A seperator does not appear before or after a null (empty) C string
+\begin{lstlisting}
+sout | 1 | "" | 2 | "" | 3 | endl;
+123
+\end{lstlisting}
+which is a local mechanism to disable insertion of the separator character.
+\item
+A seperator does not appear before a C string starting with the (extended) \Index{ASCII}\index{ASCII!extended} characters: \lstinline[mathescape=off]@([{$£¥¡¿«@
+%$
+\begin{lstlisting}[mathescape=off]
+sout | "x (" | 1 | "x [" | 2 | "x {" | 3 | "x $" | 4 | "x £" | 5 | "x ¥" | 6 | "x ¡" | 7 | "x ¿" | 8 | "x «" | 9 | endl;
+\end{lstlisting}
+%$
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+x (1 x [2 x {3 x $4 x £5 x ¥6 x ¡7 x ¿8 x «9
+\end{lstlisting}
+%$
+\item
+A seperator does not appear after a C string ending with the (extended) \Index{ASCII}\index{ASCII!extended} characters: \lstinline@,.:;!?)]}%¢»@
+\begin{lstlisting}[belowskip=0pt]
+sout | 1 | ", x" | 2 | ". x" | 3 | ": x" | 4 | "; x" | 5 | "! x" | 6 | "? x" | 7 | ") x" | 8 | "] x" | 9 | "} x"
+         | 10 | "% x" | 11 | "¢ x" | 12 | "» x" | endl;
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+1, x 2. x 3: x 4; x 5! x 6? x 7) x 8] x 9} x 10% x 11¢ 12»
+\end{lstlisting}
+\item
+A seperator does not appear before or after a C string begining/ending with the \Index{ASCII} quote or whitespace characters: \lstinline[showspaces=true]@`'" \t\v\f\r\n@
+\begin{lstlisting}[belowskip=0pt]
+sout | "x`" | 1 | "`x'" | 2 | "'x\"" | 3 | "\"x" | "x " | 4 | " x" | "x\t" | 1 | "\tx" | endl;
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,showtabs=true,aboveskip=0pt,belowskip=0pt]
+x`1`x'2'x"3"x x 4 x x   1       x
+\end{lstlisting}
+\end{enumerate}
+The following \CC-style \Index{manipulator}s allow further control over implicit seperation.
+\begin{lstlisting}[mathescape=off,belowskip=0pt]
+sout | sepOn | 1 | 2 | 3 | sepOn | endl;        // separator at start of line
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+ 1 2 3
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,aboveskip=0pt,belowskip=0pt]
+sout | 1 | sepOff | 2 | 3 | endl;                       // turn off implicit separator temporarily
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+12 3
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,aboveskip=0pt,belowskip=0pt]
+sout | sepDisable | 1 | 2 | 3 | endl;           // turn off implicit separation, affects all subsequent prints
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+123
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,aboveskip=0pt,belowskip=0pt]
+sout | 1 | sepOn | 2 | 3 | endl;                        // turn on implicit separator temporarily
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+1 23
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,aboveskip=0pt,belowskip=0pt]
+sout | sepEnable | 1 | 2 | 3 | endl;            // turn on implicit separation, affects all subsequent prints
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt,belowskip=0pt]
+ 1 2 3
+\end{lstlisting}
+\begin{lstlisting}[mathescape=off,aboveskip=0pt,aboveskip=0pt,belowskip=0pt]
+sepSet( sout, ", $" );                                          // change separator from " " to ", $"
+sout | 1 | 2 | 3 | endl;
+\end{lstlisting}
+%$
+\begin{lstlisting}[mathescape=off,showspaces=true,aboveskip=0pt]
+1, $2, $3
+\end{lstlisting}
+%$
+\begin{comment}
+#include <fstream>
+
+int main() {
+        int x = 3, y = 5, z = 7;
+        sout | x * 3 | y + 1 | z << 2 | x == y | (x | y) | (x || y) | (x > z ? 1 : 2) | endl;
+        sout | 1 | 2 | 3 | endl;
+        sout | '1' | '2' | '3' | endl;
+        sout | 1 | "" | 2 | "" | 3 | endl;
+        sout | "x (" | 1 | "x [" | 2 | "x {" | 3 | "x $" | 4 | "x £" | 5 | "x ¥" | 6 | "x ¡" | 7 | "x ¿" | 8 | "x «" | 9 | endl;
+        sout | 1 | ", x" | 2 | ". x" | 3 | ": x" | 4 | "; x" | 5 | "! x" | 6 | "? x" | 7 | ") x" | 8 | "] x" | 9 | "} x"
+                 | 10 | "% x" | 11 | "¢ x" | 12 | "» x" | endl;
+        sout | "x`" | 1 | "`x'" | 2 | "'x\"" | 3 | "\"x" | "x " | 4 | " x" | "x\t" | 1 | "\tx" | endl;
+        sout | sepOn | 1 | 2 | 3 | sepOn | endl;        // separator at start of line
+        sout | 1 | sepOff | 2 | 3 | endl;                       // turn off implicit separator temporarily
+        sout | sepDisable | 1 | 2 | 3 | endl;           // turn off implicit separation, affects all subsequent prints
+        sout | 1 | sepOn | 2 | 3 | endl;                        // turn on implicit separator temporarily
+        sout | sepEnable | 1 | 2 | 3 | endl;            // turn on implicit separation, affects all subsequent prints
+        sepSet( sout, ", $" );                                          // change separator from " " to ", $"
+        sout | 1 | 2 | 3 | endl;
+
+}
+
+// Local Variables: //
+// tab-width: 4 //
+// End: //
+\end{comment}
+%$
+
+
+\section{Standard Library}
+\label{s:StandardLibrary}
+
+The goal of the \CFA standard-library is to wrap many of the existing C library-routines that are explicitly polymorphic into implicitly polymorphic versions.
+
+
+\subsection{malloc}
+
+\begin{lstlisting}
+forall( otype T ) T * malloc( void );§\indexc{malloc}§
+forall( otype T ) T * malloc( char fill );
+forall( otype T ) T * malloc( T * ptr, size_t size );
+forall( otype T ) T * malloc( T * ptr, size_t size, unsigned char fill );
+forall( otype T ) T * calloc( size_t nmemb );§\indexc{calloc}§
+forall( otype T ) T * realloc( T * ptr, size_t size );§\indexc{ato}§
+forall( otype T ) T * realloc( T * ptr, size_t size, unsigned char fill );
+
+forall( otype T ) T * aligned_alloc( size_t alignment );§\indexc{ato}§
+forall( otype T ) T * memalign( size_t alignment );             // deprecated
+forall( otype T ) int posix_memalign( T ** ptr, size_t alignment );
+
+forall( otype T ) T * memset( T * ptr, unsigned char fill ); // use default value '\0' for fill
+forall( otype T ) T * memset( T * ptr );                                // remove when default value available
+\end{lstlisting}
+
+
+\subsection{ato / strto}
+
+\begin{lstlisting}
+int ato( const char * ptr );§\indexc{ato}§
+unsigned int ato( const char * ptr );
+long int ato( const char * ptr );
+unsigned long int ato( const char * ptr );
+long long int ato( const char * ptr );
+unsigned long long int ato( const char * ptr );
+float ato( const char * ptr );
+double ato( const char * ptr );
+long double ato( const char * ptr );
+float _Complex ato( const char * ptr );
+double _Complex ato( const char * ptr );
+long double _Complex ato( const char * ptr );
+
+int strto( const char * sptr, char ** eptr, int base );
+unsigned int strto( const char * sptr, char ** eptr, int base );
+long int strto( const char * sptr, char ** eptr, int base );
+unsigned long int strto( const char * sptr, char ** eptr, int base );
+long long int strto( const char * sptr, char ** eptr, int base );
+unsigned long long int strto( const char * sptr, char ** eptr, int base );
+float strto( const char * sptr, char ** eptr );
+double strto( const char * sptr, char ** eptr );
+long double strto( const char * sptr, char ** eptr );
+float _Complex strto( const char * sptr, char ** eptr );
+double _Complex strto( const char * sptr, char ** eptr );
+long double _Complex strto( const char * sptr, char ** eptr );
+\end{lstlisting}
+
+
+\subsection{bsearch / qsort}
+
+\begin{lstlisting}
+forall( otype T | { int ?<?( T, T ); } )
+T * bsearch( const T key, const T * arr, size_t dimension );§\indexc{bsearch}§
+
+forall( otype T | { int ?<?( T, T ); } )
+void qsort( const T * arr, size_t dimension );§\indexc{qsort}§
+\end{lstlisting}
+
+
+\subsection{abs}
+
+\begin{lstlisting}
+char abs( char );§\indexc{abs}§
+int abs( int );
+long int abs( long int );
+long long int abs( long long int );
+float abs( float );
+double abs( double );
+long double abs( long double );
+float abs( float _Complex );
+double abs( double _Complex );
+long double abs( long double _Complex );
+\end{lstlisting}
+
+
+\subsection{random}
+
+\begin{lstlisting}
+void rand48seed( long int s );§\indexc{rand48seed}§
+char rand48();§\indexc{rand48}§
+int rand48();
+unsigned int rand48();
+long int rand48();
+unsigned long int rand48();
+float rand48();
+double rand48();
+float _Complex rand48();
+double _Complex rand48();
+long double _Complex rand48();
+\end{lstlisting}
+
+
+\subsection{min / max / swap}
+
+\begin{lstlisting}
+forall( otype T | { int ?<?( T, T ); } )
+T min( const T t1, const T t2 );§\indexc{min}§
+
+forall( otype T | { int ?>?( T, T ); } )
+T max( const T t1, const T t2 );§\indexc{max}§
+
+forall( otype T )
+void swap( T * t1, T * t2 );§\indexc{swap}§
+\end{lstlisting}
+
+
+\section{Math Library}
+\label{s:Math Library}
+
+The goal of the \CFA math-library is to wrap many of the existing C math library-routines that are explicitly polymorphic into implicitly polymorphic versions.
+
+
+\subsection{General}
+
+\begin{lstlisting}
+float fabs( float );§\indexc{fabs}§
+double fabs( double );
+long double fabs( long double );
+float cabs( float _Complex );
+double cabs( double _Complex );
+long double cabs( long double _Complex );
+
+float ?%?( float, float );§\indexc{fmod}§
+float fmod( float, float );
+double ?%?( double, double );
+double fmod( double, double );
+long double ?%?( long double, long double );
+long double fmod( long double, long double );
+
+float remainder( float, float );§\indexc{remainder}§
+double remainder( double, double );
+long double remainder( long double, long double );
+
+[ int, float ] remquo( float, float );§\indexc{remquo}§
+float remquo( float, float, int * );
+[ int, double ] remquo( double, double );
+double remquo( double, double, int * );
+[ int, long double ] remquo( long double, long double );
+long double remquo( long double, long double, int * );
+
+[ int, float ] div( float, float );                                             // alternative name for remquo
+float div( float, float, int * );§\indexc{div}§
+[ int, double ] div( double, double );
+double div( double, double, int * );
+[ int, long double ] div( long double, long double );
+long double div( long double, long double, int * );
+
+float fma( float, float, float );§\indexc{fma}§
+double fma( double, double, double );
+long double fma( long double, long double, long double );
+
+float fdim( float, float );§\indexc{fdim}§
+double fdim( double, double );
+long double fdim( long double, long double );
+
+float nan( const char * );§\indexc{nan}§
+double nan( const char * );
+long double nan( const char * );
+\end{lstlisting}
+
+
+\subsection{Exponential}
+
+\begin{lstlisting}
+float exp( float );§\indexc{exp}§
+double exp( double );
+long double exp( long double );
+float _Complex exp( float _Complex );
+double _Complex exp( double _Complex );
+long double _Complex exp( long double _Complex );
+
+float exp2( float );§\indexc{exp2}§
+double exp2( double );
+long double exp2( long double );
+float _Complex exp2( float _Complex );
+double _Complex exp2( double _Complex );
+long double _Complex exp2( long double _Complex );
+
+float expm1( float );§\indexc{expm1}§
+double expm1( double );
+long double expm1( long double );
+
+float log( float );§\indexc{log}§
+double log( double );
+long double log( long double );
+float _Complex log( float _Complex );
+double _Complex log( double _Complex );
+long double _Complex log( long double _Complex );
+
+float log2( float );§\indexc{log2}§
+double log2( double );
+long double log2( long double );
+float _Complex log2( float _Complex );
+double _Complex log2( double _Complex );
+long double _Complex log2( long double _Complex );
+
+float log10( float );§\indexc{log10}§
+double log10( double );
+long double log10( long double );
+float _Complex log10( float _Complex );
+double _Complex log10( double _Complex );
+long double _Complex log10( long double _Complex );
+
+float log1p( float );§\indexc{log1p}§
+double log1p( double );
+long double log1p( long double );
+
+int ilogb( float );§\indexc{ilogb}§
+int ilogb( double );
+int ilogb( long double );
+
+float logb( float );§\indexc{logb}§
+double logb( double );
+long double logb( long double );
+\end{lstlisting}
+
+
+\subsection{Power}
+
+\begin{lstlisting}
+float sqrt( float );§\indexc{sqrt}§
+double sqrt( double );
+long double sqrt( long double );
+float _Complex sqrt( float _Complex );
+double _Complex sqrt( double _Complex );
+long double _Complex sqrt( long double _Complex );
+
+float cbrt( float );§\indexc{cbrt}§
+double cbrt( double );
+long double cbrt( long double );
+
+float hypot( float, float );§\indexc{hypot}§
+double hypot( double, double );
+long double hypot( long double, long double );
+
+float pow( float, float );§\indexc{pow}§
+double pow( double, double );
+long double pow( long double, long double );
+float _Complex pow( float _Complex, float _Complex );
+double _Complex pow( double _Complex, double _Complex );
+long double _Complex pow( long double _Complex, long double _Complex );
+\end{lstlisting}
+
+
+\subsection{Trigonometric}
+
+\begin{lstlisting}
+float sin( float );§\indexc{sin}§
+double sin( double );
+long double sin( long double );
+float _Complex sin( float _Complex );
+double _Complex sin( double _Complex );
+long double _Complex sin( long double _Complex );
+
+float cos( float );§\indexc{cos}§
+double cos( double );
+long double cos( long double );
+float _Complex cos( float _Complex );
+double _Complex cos( double _Complex );
+long double _Complex cos( long double _Complex );
+
+float tan( float );§\indexc{tan}§
+double tan( double );
+long double tan( long double );
+float _Complex tan( float _Complex );
+double _Complex tan( double _Complex );
+long double _Complex tan( long double _Complex );
+
+float asin( float );§\indexc{asin}§
+double asin( double );
+long double asin( long double );
+float _Complex asin( float _Complex );
+double _Complex asin( double _Complex );
+long double _Complex asin( long double _Complex );
+
+float acos( float );§\indexc{acos}§
+double acos( double );
+long double acos( long double );
+float _Complex acos( float _Complex );
+double _Complex acos( double _Complex );
+long double _Complex acos( long double _Complex );
+
+float atan( float );§\indexc{atan}§
+double atan( double );
+long double atan( long double );
+float _Complex atan( float _Complex );
+double _Complex atan( double _Complex );
+long double _Complex atan( long double _Complex );
+
+float atan2( float, float );§\indexc{atan2}§
+double atan2( double, double );
+long double atan2( long double, long double );
+
+float atan( float, float );                                                             // alternative name for atan2
+double atan( double, double );§\indexc{atan}§
+long double atan( long double, long double );
+\end{lstlisting}
+
+
+\subsection{Hyperbolic}
+
+\begin{lstlisting}
+float sinh( float );§\indexc{sinh}§
+double sinh( double );
+long double sinh( long double );
+float _Complex sinh( float _Complex );
+double _Complex sinh( double _Complex );
+long double _Complex sinh( long double _Complex );
+
+float cosh( float );§\indexc{cosh}§
+double cosh( double );
+long double cosh( long double );
+float _Complex cosh( float _Complex );
+double _Complex cosh( double _Complex );
+long double _Complex cosh( long double _Complex );
+
+float tanh( float );§\indexc{tanh}§
+double tanh( double );
+long double tanh( long double );
+float _Complex tanh( float _Complex );
+double _Complex tanh( double _Complex );
+long double _Complex tanh( long double _Complex );
+
+float asinh( float );§\indexc{asinh}§
+double asinh( double );
+long double asinh( long double );
+float _Complex asinh( float _Complex );
+double _Complex asinh( double _Complex );
+long double _Complex asinh( long double _Complex );
+
+float acosh( float );§\indexc{acosh}§
+double acosh( double );
+long double acosh( long double );
+float _Complex acosh( float _Complex );
+double _Complex acosh( double _Complex );
+long double _Complex acosh( long double _Complex );
+
+float atanh( float );§\indexc{atanh}§
+double atanh( double );
+long double atanh( long double );
+float _Complex atanh( float _Complex );
+double _Complex atanh( double _Complex );
+long double _Complex atanh( long double _Complex );
+\end{lstlisting}
+
+
+\subsection{Error / Gamma}
+
+\begin{lstlisting}
+float erf( float );§\indexc{erf}§
+double erf( double );
+long double erf( long double );
+float _Complex erf( float _Complex );
+double _Complex erf( double _Complex );
+long double _Complex erf( long double _Complex );
+
+float erfc( float );§\indexc{erfc}§
+double erfc( double );
+long double erfc( long double );
+float _Complex erfc( float _Complex );
+double _Complex erfc( double _Complex );
+long double _Complex erfc( long double _Complex );
+
+float lgamma( float );§\indexc{lgamma}§
+double lgamma( double );
+long double lgamma( long double );
+float lgamma( float, int * );
+double lgamma( double, int * );
+long double lgamma( long double, int * );
+
+float tgamma( float );§\indexc{tgamma}§
+double tgamma( double );
+long double tgamma( long double );
+\end{lstlisting}
+
+
+\subsection{Nearest Integer}
+
+\begin{lstlisting}
+float floor( float );§\indexc{floor}§
+double floor( double );
+long double floor( long double );
+
+float ceil( float );§\indexc{ceil}§
+double ceil( double );
+long double ceil( long double );
+
+float trunc( float );§\indexc{trunc}§
+double trunc( double );
+long double trunc( long double );
+
+float rint( float );§\indexc{rint}§
+long double rint( long double );
+long int rint( float );
+long int rint( double );
+long int rint( long double );
+long long int rint( float );
+long long int rint( double );
+long long int rint( long double );
+
+long int lrint( float );§\indexc{lrint}§
+long int lrint( double );
+long int lrint( long double );
+long long int llrint( float );
+long long int llrint( double );
+long long int llrint( long double );
+
+float nearbyint( float );§\indexc{nearbyint}§
+double nearbyint( double );
+long double nearbyint( long double );
+
+float round( float );§\indexc{round}§
+long double round( long double );
+long int round( float );
+long int round( double );
+long int round( long double );
+long long int round( float );
+long long int round( double );
+long long int round( long double );
+
+long int lround( float );§\indexc{lround}§
+long int lround( double );
+long int lround( long double );
+long long int llround( float );
+long long int llround( double );
+long long int llround( long double );
+\end{lstlisting}
+
+
+\subsection{Manipulation}
+
+\begin{lstlisting}
+float copysign( float, float );§\indexc{copysign}§
+double copysign( double, double );
+long double copysign( long double, long double );
+
+float frexp( float, int * );§\indexc{frexp}§
+double frexp( double, int * );
+long double frexp( long double, int * );
+
+float ldexp( float, int );§\indexc{ldexp}§
+double ldexp( double, int );
+long double ldexp( long double, int );
+
+[ float, float ] modf( float );§\indexc{modf}§
+float modf( float, float * );
+[ double, double ] modf( double );
+double modf( double, double * );
+[ long double, long double ] modf( long double );
+long double modf( long double, long double * );
+
+float nextafter( float, float );§\indexc{nextafter}§
+double nextafter( double, double );
+long double nextafter( long double, long double );
+
+float nexttoward( float, long double );§\indexc{nexttoward}§
+double nexttoward( double, long double );
+long double nexttoward( long double, long double );
+
+float scalbn( float, int );§\indexc{scalbn}§
+double scalbn( double, int );
+long double scalbn( long double, int );
+
+float scalbln( float, long int );§\indexc{scalbln}§
+double scalbln( double, long int );
+long double scalbln( long double, long int );
+\end{lstlisting}
+
+
+\section{Rational Numbers}
+\label{s:RationalNumbers}
+
+Rational numbers are numbers written as a ratio, i.e., as a fraction, where the numerator (top number) and the denominator (bottom number) are whole numbers.
+When creating and computing with rational numbers, results are constantly reduced to keep the numerator and denominator as small as possible.
+
+\begin{lstlisting}
+// implementation
+struct Rational {§\indexc{Rational}§
+        long int numerator, denominator;                                        // invariant: denominator > 0
+}; // Rational
+
+// constants
+extern struct Rational 0;
+extern struct Rational 1;
+
+// constructors
+Rational rational();
+Rational rational( long int n );
+Rational rational( long int n, long int d );
+
+// getter/setter for numerator/denominator
+long int numerator( Rational r );
+long int numerator( Rational r, long int n );
+long int denominator( Rational r );
+long int denominator( Rational r, long int d );
+
+// comparison
+int ?==?( Rational l, Rational r );
+int ?!=?( Rational l, Rational r );
+int ?<?( Rational l, Rational r );
+int ?<=?( Rational l, Rational r );
+int ?>?( Rational l, Rational r );
+int ?>=?( Rational l, Rational r );
+
+// arithmetic
+Rational -?( Rational r );
+Rational ?+?( Rational l, Rational r );
+Rational ?-?( Rational l, Rational r );
+Rational ?*?( Rational l, Rational r );
+Rational ?/?( Rational l, Rational r );
+
+// conversion
+double widen( Rational r );
+Rational narrow( double f, long int md );
+
+// I/O
+forall( dtype istype | istream( istype ) ) istype * ?|?( istype *, Rational * );
+forall( dtype ostype | ostream( ostype ) ) ostype * ?|?( ostype *, Rational );
+\end{lstlisting}
+
+
 \bibliographystyle{plain}
-\bibliography{/usr/local/bibliographies/pl.bib}
+\bibliography{cfa}