diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/syntax.txt | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/doc/syntax.txt b/doc/syntax.txt new file mode 100644 index 0000000000..044ba8ee5e --- /dev/null +++ b/doc/syntax.txt @@ -0,0 +1,68 @@ + +====================================================================== +Conventions lexicales +====================================================================== + + INFIX = suites de symboles speciaux, repartis en plusieurs + categories correspondant a des precedences differentes + (comme en ocaml) + + si `s' est un infix, alors `@s' est un IDENT correspondant au + symbole (prefixe) correspondant + + d'ou definition $+ := plus; + check O + O; + +====================================================================== +Constr +====================================================================== + +simple_constr + ::= qident + | "\" binders "." constr \\ lambda + | "!" binders "." constr \\ produit + | constr "->" constr \\ assoc droite + | "(" simple_constr+ ")" + | "cases" constr "of" OPT "|" LIST0 equation SEP "|" "end" + | "fix" ident "where" LIST1 recursive SEP "and" + | "Set" + | "Prop" + | "Type" + | "?" + | constr infix constr \\ =, +, -, *, /, **, ++, etc. + \\ /\ and ? \/ or ? + | "~" constr \\ not ? + +constr + ::= simple_constr+ + +binders + ::= LIST1 ident SEP "," + | LIST1 binder SEP "," + +binder + ::= LIST1 ident SEP "," ":" constr + +equation + ::= pattern "=>" constr + +pattern + ::= + +recursive + ::= ident binders "{" "struct" ident "}" ":" constr ":=" constr + + +====================================================================== +Tactic +====================================================================== + + +====================================================================== +Vernac +====================================================================== + +vernac + ::= "definition" ... + | "fixpoint" LIST1 recursive SEP "and" + |