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

doc: syntax of theories (start)

parent 6c2c5eff
......@@ -749,7 +749,7 @@ clean::
DOC = doc/manual.pdf
# doc/manual.html
BNF = qualid term formula
BNF = qualid type term formula theory
BNFTEX = $(addprefix doc/, $(addsuffix _bnf.tex, $(BNF)))
doc/%_bnf.tex: doc/%.bnf doc/bnf
......@@ -5,29 +5,46 @@ This chapter gives the grammar for the input files.
TODO: constants
\paragraph{Identifiers.} The syntax distinguishes lowercase and
uppercase identifiers and, consequently, lowercase and uppercase
qualified identifiers.
The syntax of terms is given Figure~\ref{fig:bnf:term}.
\paragraph{Type Expressions.} The syntax for type
expressions notably differs from the usual ML syntax.
\paragraph{Terms and Types.}
The syntax for terms is given Figure~\ref{fig:bnf:term}.
Note the curryfied syntax for function application, though partial
application is not allowed (rejected at typing).
TODO: prefix and infix operators
\caption{Syntax of terms.}
\caption{Syntax for terms.}
The syntax of terms is given Figure~\ref{fig:bnf:formula}.
The syntax for formulas is given Figure~\ref{fig:bnf:formula}.
\caption{Syntax of formulas.}
\caption{Syntax for formulas.}
\caption{Syntax for theories.}
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
theory ::= "theory" uident label* decl* "end"
decl ::= %
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