Commit 2c8012f0 authored by MARCHE Claude's avatar MARCHE Claude

fix bnf in doc

parent cfe30054
...@@ -44,4 +44,5 @@ ...@@ -44,4 +44,5 @@
\ \
handler ::= uqualid pattern? "->" expr handler ::= uqualid pattern? "->" expr
\ \
to-downto ::= "to" | "downto"
\end{syntax} \end{syntax}
...@@ -8,6 +8,5 @@ ...@@ -8,6 +8,5 @@
binder ::= "ghost"? lident label* binder ::= "ghost"? lident label*
| param | param
\ \
param ::= "(" ("ghost"? lident label*)+ ":" type ")" ; param ::= "(" ("ghost"? lident label*)+ ":" type ")"
\
\end{syntax} \end{syntax}
...@@ -25,6 +25,5 @@ ...@@ -25,6 +25,5 @@
| "=" "fun" binder+ spec* "->" spec* expr ; | "=" "fun" binder+ spec* "->" spec* expr ;
\ \
pgm-decl ::= ":" type ; global variable pgm-decl ::= ":" type ; global variable
| param (spec* param)+ ":" type spec* ; abstract function | param (spec* param)+ ":" type spec* ; abstract function%
\
\end{syntax} \end{syntax}
...@@ -27,5 +27,4 @@ ...@@ -27,5 +27,4 @@
\ \
assertion ::= ("assert" | "assume" | "check") "{" formula "}" ; assertion ::= ("assert" | "assume" | "check") "{" formula "}" ;
| "absurd" | "absurd"
\
\end{syntax} \end{syntax}
...@@ -186,13 +186,13 @@ The syntax for program expressions is given in ...@@ -186,13 +186,13 @@ The syntax for program expressions is given in
Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}. Figure~\ref{fig:bnf:expra} and~Figure~\ref{fig:bnf:exprb}.
\begin{figure} \begin{figure}
\begin{center}\framebox{\input{./expr_bnf.tex}}\end{center} \begin{center}\framebox{\input{./expr_bnf.tex}}\end{center}
\caption{Syntax for program expressions (part1).} \caption{Syntax for program expressions (part 1).}
\label{fig:bnf:expra} \label{fig:bnf:expra}
\end{figure} \end{figure}
\begin{figure} \begin{figure}
\begin{center}\framebox{\input{./expr2_bnf.tex}}\end{center} \begin{center}\framebox{\input{./expr2_bnf.tex}}\end{center}
\caption{Syntax for program expressions (part2).} \caption{Syntax for program expressions (part 2).}
\label{fig:bnf:exprb} \label{fig:bnf:exprb}
\end{figure} \end{figure}
...@@ -354,6 +354,7 @@ A theory defined in a \whyml\ file can only be used within that ...@@ -354,6 +354,7 @@ A theory defined in a \whyml\ file can only be used within that
file. If a theory is supposed to be reused from other files, be they file. If a theory is supposed to be reused from other files, be they
\why\ or \whyml\ files, it should be defined in a \why\ file. \why\ or \whyml\ files, it should be defined in a \why\ file.
%%% Local Variables: %%% Local Variables:
%%% mode: latex %%% mode: latex
%%% TeX-PDF-mode: t %%% TeX-PDF-mode: t
......
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