fixed documentation for axiom/lemma/goal names

syntax for inductive-decl
parent 53db8e7c
......@@ -4,9 +4,9 @@
decl ::= "type" type-decl ("with" type-decl)* ;
| "logic" logic-decl ("with" logic-decl)* ;
| "inductive" inductive-decl ("with" inductive-decl)* ;
| "axiom" uident ":" formula ;
| "lemma" uident ":" formula ;
| "goal" uident ":" formula ;
| "axiom" ident ":" formula ;
| "lemma" ident ":" formula ;
| "goal" ident ":" formula ;
| "use" imp-exp tqualid ("as" uident-opt)? ;
| "clone" imp-exp tqualid ("as" uident-opt)? subst? ;
| "namespace" "import"? uident-opt decl* "end" ;
......@@ -33,6 +33,11 @@
| "(" type ("," type)* ")" ;
| "()"
\
inductive-decl ::= lident label* type-param* "=" ;
"|"? ind-case ("|" ind-case)* ;
\
ind-case ::= ident label* ":" formula ;
\
imp-exp ::= ("import" | "export")?
\
uident-opt ::= uident | "_"
......
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