diff options
| author | filliatr | 2000-12-12 22:44:30 +0000 |
|---|---|---|
| committer | filliatr | 2000-12-12 22:44:30 +0000 |
| commit | 4e283e52a29ba769b4b18fd26145924a40b21ec6 (patch) | |
| tree | 5073e67d3857b03a224e8c9928e6e6a94a1975b9 /doc | |
| parent | b6018c78b25da14d4f44cf10de692f968cba1e98 (diff) | |
fichier proposition syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8145 85f007b7-540e-0410-9357-904b9bb8a0f7
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" + |