LP, the Larch Prover -- Syntax descriptions
The syntax of LP is described using equations of the form
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.
<term> ::= <simpleId> | <simpleId> "(" <term>+, ")"
- chars or "chars"
- A terminal symbol
- 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
- An e as a syntactic unit, as in (e | f) e. Without
parentheses, e | f e is interpreted as e | (f e).
- An optional e
- e* or e*, or e*[,]
- Zero or more e's, separated respectively by nothing, commas, or
- e+ or e+, or e+[,]
- One or more e's, separated respectively by nothing, commas, or