Commit 74c29c96 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix broken links.

parent 9d26e427
......@@ -189,8 +189,8 @@ constructed.
Here is the way we build the formula $2+2=4$. The main difficulty is to
access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see
Chap~\ref{sec:library}).
the standard theory \texttt{Int} of the file \texttt{int.why}.
% (see Chap~\ref{sec:library}).
\lstinputlisting{generated/logic__buildfmla.ml}
An important point to notice as that when building the application of
$+$ to the arguments, it is checked that the types are correct. Indeed
......
......@@ -118,8 +118,14 @@ extraction command line:
\paragraph{Examples.}
We illustrate different ways of using the \texttt{extract} command through some
examples. Consider the program in Figure~\ref{fig:AQueue} on
page~\pageref{fig:AQueue}. If we are only interested in extracting function
examples.
\begin{latexonly}
Consider the program in Figure~\ref{fig:AQueue} on page~\pageref{fig:AQueue}.
\end{latexonly}
\begin{htmlonly}
Consider the program of Section~\ref{sec:AQueue}.
\end{htmlonly}
If we are only interested in extracting function
\texttt{enqueue}, we can proceed as follows:
\begin{verbatim}
> why3 extract -D ocaml64 -L . aqueue.AmortizedQueue.enqueue -o aqueue.ml
......
......@@ -931,6 +931,7 @@ end
%END LATEX
\section{Problem 5: Amortized Queue}
\label{sec:AQueue}
The last problem consists in verifying the implementation of a
well-known purely applicative data structure for queues.
......
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