Fixity declaration

From The Twelf Project
Jump to: navigation, search

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.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 %%


See also



This page is incomplete. We should expand it.