Fixity declaration
From The Twelf Project
The %infix, %prefix and %postfix declarations assign fixity and precedence to constants for the purpose of parsing (they have no meaning in the logic).
| This article or section needs a description of the syntax. |
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.5R3, Aug 30, 2005 (%trustme)x : a = (b + c) * d. y : a = b + c * d.
%% OK %%
[edit] See also
- Operator Declaration in the User's Guide
This page is incomplete. We should expand it.
