LP, the Larch Prover -- Precedence

Parsing

When parsing a term, LP binds some operators more tightly than others, thereby reducing the need for parentheses. The operators in the following list bind increasingly tightly:

if __ then __ else __
<=>
=>
/\ and \/
= and ~=
All infix, postfix, and prefix operators not otherwise mentioned in this list
Postfix selection operators (of the form .<simpleId>) and . as an infix operator

Parentheses are required elsewhere to specify associativity, except that terms such as t1 + t2 + ... + tn, which involve a sequence of terms separated by a single infix identifier (other than =>, =, and ~=), do not need parentheses and are associated to the left.

Quantifiers bind more tightly than all operators.

Examples

Unparenthesized version    Interpretation
----------------------     --------------
a < b + c                  Error
p /\ q \/ r                Error
p => q => r                Error
x - y - z                  (x - y) - z
a = b + c => b < s(a)      (a = (b + c)) => (b < s(a))
a.b.c!                     ((a.b).c)!
~p /\ ~x.pre               (~p) /\ (~(x.pre))
\E x (x < c) => c > 0      (\E x (x < c)) => (c > 0)
\A x \E y x < y            (\A x \E y x) < y

Ordering

When orienting formulas into rewrite rules, LP sometimes uses a partial ordering on operators that is known in the literature as a precedence relation. See register.