Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
2103b6b8
Commit
2103b6b8
authored
Dec 15, 2010
by
Jean-Christophe Filliâtre
Browse files
doc: syntax for lists with separators
parent
f7511358
Changes
4
Hide whitespace changes
Inline
Side-by-side
doc/formula.bnf
View file @
2103b6b8
...
...
@@ -14,10 +14,10 @@
| "if" formula "then" formula ;
"else" formula ; conditional
| "let" pattern "=" term "in" formula ; local binding
| "match" ("," term)+ "with" ;
"|"?
("|" formula-case)+ "end" ; pattern matching
| quantifier ("," binders )
+
;
triggers? "." formula ; quantifier
| "match"
term
("," term)+ "with" ;
("|" formula-case)+ "end" ; pattern matching
| quantifier
binders
("," binders )
*
;
triggers? "." formula
; quantifier
| label formula ; label
| "(" formula ")" ; parentheses
\
...
...
@@ -25,9 +25,11 @@
\
binders ::= lident+ ":" type
\
triggers ::= "[" ("|" trigger)
+
"]" ;
triggers ::= "["
trigger
("|" trigger)
*
"]" ;
\
trigger ::= ("," (term | formula))+;
trigger ::= tr-term ("," tr-term)* ;
\
tr-term ::= term | formula ;
\
formula-case ::= pattern "->" formula ; %
\end{syntax}
doc/term.bnf
View file @
2103b6b8
...
...
@@ -9,9 +9,9 @@
"else" term ; conditional
| "let" pattern "=" term "in" term
; local binding
| "match" ("," term)
+
"with" ;
"|"?
("|" term-case)+ "end" ; pattern matching
| "(" term ("," term)
*
")" ; tuple
| "match"
term
("," term)
*
"with" ;
("|" term-case)+ "end"
; pattern matching
| "(" term ("," term)
+
")" ; tuple
| term ":" type ; cast
| label term ; label
| "(" term ")" ; parentheses
...
...
doc/theory.bnf
View file @
2103b6b8
\begin{syntax}
theory ::= "theory" uident label* decl* "end"
\
decl ::= "type" ("with" type-decl)
+
;
| "logic" ("with" logic-decl)
+
;
| "inductive" ("with" inductive-decl)
+
;
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 ;
...
...
@@ -23,5 +23,5 @@
| "lemma" uqualid ;
| "goal" uqualid ;
\
tqualid ::= uident | ("." ident)
+
"." uident ; %
tqualid ::= uident |
ident
("." ident)
*
"." uident ; %
\end{syntax}
doc/type.bnf
View file @
2103b6b8
\begin{syntax}
type ::= lqualid type* ; type symbol
| "'" lident ; type variable
| "(" ("," type)* ")" ; tuple type
| "()" ; empty tuple type
| "(" type ("," type)+ ")" ; tuple type
| "(" type ")" ; parentheses %
\end{syntax}
\ No newline at end of file
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment