Commit 7ce19416 authored by Francois Bobot's avatar Francois Bobot

un peu de definition de syntax

parent d6f9d489
......@@ -132,6 +132,24 @@ Keywords are the following:
\end{center}
\section{Grammar}
%% file := decl*
%% decl := | "theory" uident decl* "end"
%% | "theory" uident "." uqualid ("with" instance+ )?
%% | "use" "open"? uqualid ("as" ident)
%% | "use" "include" uqualid %% pas de as pour include
%% | ("axiom"|"lemma"|"goal") ident ":" fmla
%% | "type" typarams lident ("=" (ty-alg | ty))?
%% ("and" typarams lident ("=" (ty-alg | ty))?)*
%% Il faut verifier qu'il y a toujours un constructeur entre deux
%% définitions récursives.
%% | "logic" def ("and" def)*
%% | "inductive" ...
%% def := lident_ou_infix ("(" formal+, ")")? (":" ty)? ("=" lexpr)?
%% formal := ((lident|_)":")? ty
%% instance := | lqualid "=" lqualid
%% ty-alg := | uident ("(" ty,+ ")")? ("|" uident ...)*
\subsection{Qualified names}
......
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