The %infix, %prefix and %postfix declarations assign fixity and precedence to constants for the purpose of parsing (they have no meaning in the logic).
Higher numbers bind tighter, and the pretty printer only prints out necessary information. Hence the following example:
a : type. b : a. c : a. d : a. + : a -> a -> a. %infix left 1 +. * : a -> a -> a. %infix left 2 *.
x : a = (b + c) * d. %% The parenthesis are necessary here y : a = b + (c * d). %% This means the same thing as b + c * d.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)
x : a = (b + c) * d. y : a = b + c * d.%% OK %%
This page is incomplete. We should expand it.