blob: 044ba8ee5ea24dd4e563372f422126ab9f5a6a56 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
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"
|
