Commit e7666870 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

doc: typos

parent 5542328b
......@@ -67,7 +67,7 @@ length. The \texttt{use import List} command indicates that this new
theory may refer to symbols from theory \texttt{List}. These symbols
are accessible in a qualified form, such as \texttt{List.list} or
\texttt{List.Cons}. The \texttt{import} qualifier additionally allows
use to use them without qualification.
us to use them without qualification.
Similarly, the next command \texttt{use import int.Int} adds to our
context the theory \texttt{int.Int} from the standard library. The
......@@ -76,7 +76,7 @@ containing theory \texttt{Int}. Theories referred to without prefix
either appear earlier in the current file, \eg\ \texttt{List}, or are
predefined.
The next declaration defines a recursive function, \emph{length},
The next declaration defines a recursive function, \texttt{length},
which computes the length of a list. The \texttt{logic} keyword is
used to introduce or define both function and predicate symbols.
\why\ checks every recursive, or mutually recursive, definition for
......@@ -115,7 +115,7 @@ declarations of another theory, coming either from the same input
text or from the library. Another way to referring to a theory is
by ``cloning''. A \texttt{clone} declaration constructs a local
copy of the cloned theory, possibly instantiating some of its
abstract (i.e.~declared but not defined) symbols.
abstract (\emph{i.e.}~declared but not defined) symbols.
\begin{figure}
\centering
......@@ -177,7 +177,7 @@ use of it (see Section~\ref{sec:drivers}).
Notice an important difference between \texttt{use}
and \texttt{clone}. If we \texttt{use} a theory, say
\texttt{List}, twice (directly or indirectly: e.g.~by
\texttt{List}, twice (directly or indirectly: \emph{e.g.}~by
making \texttt{use} of both \texttt{Length} and
\texttt{Sorted}), there is no duplication: there is
still only one type of lists and a unique pair
......@@ -194,7 +194,7 @@ this time we use the abstract order on the values of type
Now, we can instantiate theory \texttt{SortedGen} to any
ordered type, without having to retype the definition of
\texttt{sorted}. For example, theory \texttt{SortedIntList}
makes \texttt{clone} of \texttt{SortedGen} (i.e.~copies its
makes \texttt{clone} of \texttt{SortedGen} (\emph{i.e.}~copies its
declarations) substituting type \texttt{int} for type
\texttt{O.t} of \texttt{SortedGen} and the default order
on integers for predicate \texttt{O.(<=)}. \why\ will
......@@ -268,7 +268,7 @@ optional, if it is omitted, the name of the symbol is \texttt{List.$s$}.
\item \texttt{use import List as L} --- every symbol $s$ from
\texttt{List} is accessible under the name \texttt{L.$s$}. It is also
accessible simply as \texttt{$s$}, but only up to the end of the current
namespace, e.g.~the current theory. If the current theory, that is the
namespace, \emph{e.g.}~the current theory. If the current theory, that is the
one making \texttt{use}, is later used under the name \texttt{T},
the name of the symbol would be \texttt{T.L.$s$}. (This is why we
could refer directly to the symbols of \texttt{Order} in theory
......@@ -298,7 +298,7 @@ this feature is rarely used.
We now consider another, slightly more complex example: to use \why\
to solve a little puzzle known as ``Einstein's logic
problem''\footnote{This was contributed by St\'ephane Lescuyer.}.
problem''\footnote{This \why\ example was contributed by St\'ephane Lescuyer.}.
The problem is stated as follows. Five persons, of five
different nationalities, live in five houses in a row, all
painted with different colors.
......
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