Commit f2b4d068 authored by MARCHE Claude's avatar MARCHE Claude

page settings

parent 2ec97d0e
......@@ -46,7 +46,7 @@ It is not mandatory to install \why\ to use it. Local use is obtained via
./configure --enable-local
make
\end{verbatim}
The \why\ executables are then available in subdirectory \texttt{bin/}.
The \why\ executables are then available in the subdirectory \texttt{bin/}.
\subsection{Installation of the \why\ library}
\label{sec:installlib}
......@@ -277,7 +277,7 @@ the syntax of WhyML programs is intentionally left undocumented since
it might evolve significantly in the near future.
For those who want to experiment with it, examples are provided in
\texttt{examples/programs}. The files \texttt{*.mlw} can be loaded in
\texttt{examples/\ programs}. The files \texttt{*.mlw} can be loaded in
the GUI.
[TO BE COMPLETED LATER]
......@@ -302,7 +302,7 @@ comparison in various formats :
\end{itemize}
The compared composants can be defined in an \emph{rc-file},
\texttt{examples/programs/prgbench.rc} is such an example. More
\texttt{examples/programs/\ prgbench.rc} is such an example. More
generally a bench configuration file :
\begin{verbatim}
[probs "myprobs"]
......
......@@ -12,6 +12,13 @@
\setheadfoot{15pt}{38pt}
\checkandfixthelayout
% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
......@@ -30,7 +37,7 @@
\begin{document}
\sloppy
\hbadness=1100
\hbadness=1000
\thispagestyle{empty}
......
......@@ -26,7 +26,7 @@ Integer and real constants have arbitrary precision.
Integer constants may be given in base 16, 10, 8 or 2.
Real constants may be given in base 16 or 10.
\begin{figure}[p]
\begin{figure}
\begin{center}\framebox{\input{./constant_bnf.tex}}\end{center}
\caption{Syntax for constants.}
\label{fig:bnf:constant}
......@@ -73,7 +73,7 @@ associativities, from lowest to greatest priority:
Note the curryfied syntax for function application, though partial
application is not allowed (rejected at typing).
\begin{figure}[p]
\begin{figure}
\begin{center}\framebox{\input{./term_bnf.tex}}\end{center}
\caption{Syntax for terms.}
\label{fig:bnf:term}
......@@ -109,12 +109,19 @@ associativities, from lowest to greatest priority:
Note that infix symbols of level 1 include equality (\texttt{=}) and
disequality (\texttt{<>}).
\begin{figure}[p]
\begin{figure}
\begin{center}\framebox{\input{./formula_bnf.tex}}\end{center}
\caption{Syntax for formulas.}
\label{fig:bnf:formula}
\end{figure}
Notice that there are two symbols for the conjunction: \texttt{and}
and \verb|/\|, and similarly for disjunction. There are logically
equivalent, but may be treated slightly differently by some
transformation, \eg{} the \texttt{split} transformation transforms
$A~\texttt{and}~B$ into subgoals $A$ and $B$, whereas it transforms
$A~\verb|/\|~B$ into subgoals $A$ and $A\rightarrow B$.
\paragraph{Theories.}
The syntax for theories is given Figure~\ref{fig:bnf:theory}.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment