mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-30 23:45:23 +03:00
Remove index entries and text about non-existent :i, :p commands.
This commit is contained in:
parent
dd2c4b6507
commit
6201415c66
@ -1153,7 +1153,7 @@ following examples illustrate:
|
||||
\note{This is the reason why we have to use the {\tt :set ascii=on}
|
||||
command to print ASCII strings. Otherwise, Cryptol will not have
|
||||
enough information to tell numbers from
|
||||
characters.\indSettingASCII\indCmdPrint}
|
||||
characters.\indSettingASCII}
|
||||
|
||||
\noindent Since characters are simply 8-bit words, you can do word
|
||||
operations on them; including arithmetic:
|
||||
|
@ -57,21 +57,6 @@ property to apply to only 8-bit values. As usual, the type signature
|
||||
is optional.\indSignature If not given, Cryptol will infer one for
|
||||
you.
|
||||
|
||||
\begin{Exercise}\label{ex:thm:intro}
|
||||
Put the above property in a file and load it into Cryptol. Then
|
||||
issue the command:
|
||||
\begin{Verbatim}
|
||||
Cryptol> :t sqDiffsCorrect
|
||||
\end{Verbatim}
|
||||
What do you see?\indCmdInfo
|
||||
\end{Exercise}
|
||||
\begin{Answer}\ansref{ex:thm:intro}
|
||||
Cryptol will print the property location, name, and the type. The
|
||||
command {\tt :i} stands for {\tt info}. It provides data about the
|
||||
properties, type-synonyms, etc. available at the top-level of your
|
||||
program.\indCmdInfo
|
||||
\end{Answer}
|
||||
|
||||
\note{It is important to emphasize that the mathematical equality
|
||||
above and the Cryptol property are \emph{not} stating precisely the
|
||||
same property. Remember that all Cryptol arithmetic is
|
||||
|
@ -158,8 +158,6 @@
|
||||
\newcommand{\indCmdEdit}{\index{commands!edit@\texttt{:e}\ (edit)}\xspace}
|
||||
\newcommand{\indCmdHelp}{\index{commands!help@\texttt{:?}\ (help)}\xspace}
|
||||
\newcommand{\indCmdQuit}{\index{commands!quit@\texttt{:q}\ (quit)}\xspace}
|
||||
\newcommand{\indCmdPrint}{\index{commands!print@\texttt{:p}\ (print)}\xspace}
|
||||
\newcommand{\indCmdInfo}{\index{commands!info@\texttt{:i}\ (info)}\xspace}
|
||||
\newcommand{\indCmdProve}{\index{commands!prove@\texttt{:prove}}\xspace}
|
||||
\newcommand{\indCmdCheck}{\index{commands!check@\texttt{:check}}\xspace}
|
||||
\newcommand{\indCmdAutoCheck}{\index{commands!check@\texttt{:check}!automatic}\xspace}
|
||||
|
Loading…
Reference in New Issue
Block a user