Notation

The last two chapters wrote expressions by applying constructors, as in imp a (imp b a). A notation declaration lets that same expression be written a -> (b -> a).

The parser uses notation to read expressions. Aufbau also uses it to format expressions for display. It changes how a math string may be written, but the result is still a tree of term constructors. In a theory that declares a notation, the notation and constructor-application forms are interchangeable everywhere.

Infix operators

infixl and infixr make a two-argument constructor into an infix operator at a given precedence.

A higher precedence binds more tightly, so /\ at 30 groups before -> at 25. infixr associates to the right and infixl to the left. Each lemma below states one spelling against the other and closes with iff_refl, which succeeds only if the two are the same expression.

An infix precedence must be below max, and a token may be declared at only one precedence. If two infix operators have the same precedence, they must associate the same way. An infixl and an infixr declared at the same precedence will be rejected. Operators sharing an associativity and precedence level can be mixed freely, so with /\ and \/ both infixl at 30, a /\ b \/ c is (a /\ b) \/ c.

Prefix operators

prefix creates an operator written before its argument. Prefix operators also have a precedence: ~ at 40 binds more tightly than /\ at 30, so ~ a /\ b means (~ a) /\ b.

Precedence also decides whether a prefix operator’s argument needs parentheses around it. Repeated application of a prefix operator never needs parentheses.

Delimiters

Sorts and terms introduced delimiters. Math strings are split on whitespace first; delimiter characters then split the pieces further. The characters can be given as one list or as separate left and right lists.

delimiter $ ( ) $;          -- both
delimiter $ ( $ $ ) $;      -- left, then right

A left delimiter splits after itself and a right delimiter before itself; a character in the one-list form does both. Grouping therefore needs ( on the left and ) on the right. Declaring them the other way round leaves something like (imp a single token.

Delimiters must be a single byte. delimiter $ ( ) λ $; is rejected, which is why a lambda is written λ x. e and not λx. e — λ cannot be declared a delimiter to separate it from adjacent text.

Notation for everything else

notation covers constants, binders, and mixfix operators, whose notation places fixed tokens before, between, or after arguments. It lists the declaration’s variables interleaved with constants, each constant written (token:prec).

The first literal must be a constant, and it may not be shared with any other notation. . is listed as a delimiter so that x. splits into two tokens.

When a string parses as something else

A binder notation’s trailing slot is parsed with the precedence declared on the leading constant, so λ x. x + x is (λ x. x) + x in the small theory above:

+ has precedence 30, which is less than the leading constant’s 41, so the body is just x and the sum is formed around the lambda rather than inside it. The ($.$:0) in the declaration is the precedence of the . token and does not extend the body past +. Parentheses give the intended reading:

Alternative notations

A constructor can carry more than one notation. The theories in this manual declare an ASCII and a Unicode form of each operator at the same precedence:

infixr imp: $->$ prec 25;
infixr imp: $→$ prec 25;

Both parse to imp, so a proof may use whichever reads better or is easier to type. A rule stated with one applies to a goal written with the other.