17 lines
308 B
BNF
17 lines
308 B
BNF
F ::= EXISTS
|
|
EXISTS ::= exists var FORALL | FORALL
|
|
FORALL ::= forall var IMP | IMP
|
|
IMP ::= OR imp OR
|
|
OR ::= AND (or AND)*
|
|
AND ::= NOT (and NOT)*
|
|
NOT ::= not? GROUP
|
|
GROUP ::= PRED | opar F cpar
|
|
PRED ::= pred opar TERM (comma TERM)* cpar
|
|
|
|
TERM ::=
|
|
| var
|
|
| const
|
|
| FUN
|
|
|
|
FUN ::= var opar TERM (comma TERM)* cpar
|