The default order of operations is that all operators have the same precedence and associate to the right as far as possible. The user can set the precedence of an operator (and reset it at any time). Parentheses ( ) may be freely used in user-entered terms; unneeded parentheses are not displayed by the prover. The precedence of an operator is a non-negative integer; higher integers represent operators which bind more tightly, and the choice of left or right association for binary operators is determined by the parity of the precedence (even associates to the right, odd to the left).
As noted above, a prefix operator is always regarded as an abbreviation for a binary operator with the same shape with a default left argument depending on the operator. Default left arguments for operators can be set individually by the user.
The simplest use of the variable binding context is as a constant function constructor, when the bound variable is not present.
Limited higher-order matching is now available. At level 1 (?1 free) the term ?f @ ?1 matches any level 1 term: ``?f'' will match the result of binding this term with brackets. Similarly, substitution of a function defined by a variable binding context for ?f in this term will actually cause the ``unbinding'' of the function. Terms of the forms ?f@?2 have similar privileges at level 2 (?2 free), and similarly for each level. This allows the direct proof of a theorem equivalent to the built-in theorem VALUE. When new variables are introduced by theorems, they are introduced as functions of the appropriate bound variable for the level at which they are introduced (this prevents the application of theorems which introduce new variables in cases where a stratification error would be introduced; this is an unintended side-effect, but it is fairly easy to work around by replacing theorems which introduce new variables with theorems to which the values of the new variables are supplied as parameters).