1.10 Notation and Infix Operators

Lean notation is ordinary syntax attached to ordinary declarations. Operators such as +, *, =, ∧, and -> are not separate from the language of terms. They are parsed into expressions that the elaborator checks using types, namespaces, and instances.

Problem

You want to read and define notation, understand precedence and associativity, and avoid ambiguity when operators appear in programs and proofs.

Solution

Use existing notation when it improves clarity, and inspect the underlying declaration when the notation becomes unclear.

#check Nat.add
#check (2 + 3)
#eval 2 + 3

The expression:

2 + 3

is notation for an addition operation. The exact operation is chosen from the expected type and available typeclass instances.

Function Notation

Every infix operator ultimately elaborates to an expression. For example:

#eval Nat.add 2 3
#eval 2 + 3

Both evaluate to:

5

The second form is easier to read, but the first form exposes the function being used.

This matters when debugging. If notation hides the operator, use #check:

#check HAdd.hAdd
#check (2 + 3)

Lean’s overloaded notation for addition is implemented through typeclass machinery.

Infix Operators

An infix operator appears between two operands.

#eval 2 + 3
#eval 10 - 4
#eval 3 * 5

Expected results:

5
6
15

Infix notation improves readability when the operation is naturally binary.

Common examples:

Precedence

Precedence controls grouping when parentheses are omitted.

#eval 2 + 3 * 4
#eval (2 + 3) * 4

Expected results:

14
20

Multiplication binds more tightly than addition, so:

2 + 3 * 4

is parsed as:

2 + (3 * 4)

Use parentheses when precedence might distract from the main point.

Associativity

Associativity controls grouping for repeated operators of the same precedence.

For natural-number addition:

#check 1 + 2 + 3

This is parsed as:

(1 + 2) + 3

Many arithmetic operators associate to the left.

Function arrows associate to the right:

Nat -> Nat -> Nat

means:

Nat -> (Nat -> Nat)

Function application associates to the left:

f x y

means:

(f x) y

These conventions explain currying and partial application.

Prefix and Postfix Notation

A prefix operator appears before its argument.

#check -3

A postfix operator appears after its argument. Some libraries define postfix notation for special operations. In ordinary beginner Lean code, infix and prefix notation occur more often.

Logical negation is prefix notation:

#check Not
#check ¬ True

The expression:

¬ P

means:

Not P

Custom Infix Notation

You can define custom notation for a function.

def maxNat (x y : Nat) : Nat :=
  if x ≤ y then y else x

infixl:65 " ⊔ₙ " => maxNat

Use it:

#eval 3 ⊔ₙ 7
#eval 9 ⊔ₙ 4

Expected results:

7
9

The declaration:

infixl:65 " ⊔ₙ " => maxNat

means:

• infixl declares a left-associative infix operator
• 65 is the precedence level
• " ⊔ₙ " is the concrete syntax
• maxNat is the function used after parsing

Associativity Choices

Lean supports several associativity forms:

Left associative notation is suitable for arithmetic-like operations.

infixl:65 " +ₙ " => Nat.add

Right associative notation is suitable for function arrows, cons-like operators, and nested constructions.

Non-associative notation avoids unclear chains.

Custom Prefix Notation

A prefix notation can be defined similarly.

def squareNat (n : Nat) : Nat :=
  n * n

prefix:80 "□ " => squareNat

#eval □ 5

Expected result:

25

The precedence controls how much of the following expression is captured by the prefix operator.

Local Notation

Custom notation can be limited to a namespace or section.

section

def combine (x y : Nat) : Nat :=
  x + y + 1

infixl:65 " ⋄ " => combine

#eval 2 ⋄ 3

end

After the section ends, the notation is no longer available.

This is useful for examples and experiments. For public libraries, global notation should be introduced carefully.

Notation and Namespaces

Notation may refer to names inside namespaces.

namespace Myproj

def join (x y : String) : String :=
  x ++ y

infixl:65 " <+> " => join

end Myproj

Depending on how notation is declared and imported, the notation may be available when the module is imported. The underlying name remains qualified:

Myproj.join

Use namespace-aware names to avoid collisions.

Notation in Propositions

Logical notation is central in theorem statements.

theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left

Here:

P ∧ Q

is notation for conjunction, and:

P -> Q

is notation for implication.

The theorem can also be read as a function from proofs of P ∧ Q to proofs of Q ∧ P.

Notation in Types

Notation is also common in type expressions.

#check Nat × String
#check Nat -> String
#check List Nat

The product type:

Nat × String

represents pairs whose first component is a natural number and whose second component is a string.

The function type:

Nat -> String

represents functions from natural numbers to strings.

Parentheses as Documentation

Parentheses are not only for the parser. They also help readers.

Prefer:

(P ∧ Q) -> R

when the grouping matters.

Avoid relying on precedence in theorem statements that introduce new concepts. In cookbook examples, clarity is more valuable than brevity.

Recipe: Debug a Notation Problem

When notation does not behave as expected, follow this sequence.

First, check the expression:

#check (2 + 3)

Second, expose relevant declarations:

#check HAdd.hAdd
#check Nat.add

Third, add type ascriptions:

#check ((2 : Nat) + (3 : Nat))
#check ((2 : Int) + (3 : Int))

Fourth, add parentheses to force grouping:

#eval (2 + 3) * 4

This separates parsing problems from typeclass inference problems.

Common Pitfalls

If an overloaded operator is ambiguous, add a type ascription.

If an expression groups incorrectly, add parentheses.

If custom notation conflicts with existing notation, use a more specific symbol or keep the notation local.

If a custom operator behaves strangely in chains, check whether it should be infixl, infixr, or non-associative.

If notation hides the actual function, inspect the underlying declaration with #check.

Takeaway

Notation is a parsing layer over ordinary Lean expressions. Infix, prefix, and custom notation can improve readability, but they also introduce precedence, associativity, and overloading concerns. Use notation for stable, familiar operations; use explicit names, type ascriptions, and parentheses when precision matters.