LP, the Larch Prover -- Syntax descriptions
The syntax of LP is described using equations of the form
<term> ::= <simpleId> | <simpleId> "
(
" <term>+, "
)
"
that are interpreted according to the following conventions to mean that a <term> is either a simple identifier or a simple identifier followed by a parenthesized list of terms separated by commas.
chars
or "
chars
"
A terminal
symbol
<chars>
A construct defined by a syntax equation
e
f
An
e
followed by (whitespace and) an
f
e
|
f
An
e
or an
f
e
~
f
An
e
that is not an
f
(
e
)
An
e
as a syntactic unit, as in (
e
|
f
)
e
. Without parentheses,
e
|
f
e
is interpreted as
e
| (
f
e
).
[
e
]
An optional
e
e
* or
e
*, or
e
*[,]
Zero or more
e
's, separated respectively by nothing, commas, or optional commas.
e
+ or
e
+, or
e
+[,]
One or more
e
's, separated respectively by nothing, commas, or optional commas.