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

```lean id="y5p8g7"
#check Nat.add
#check (2 + 3)
#eval 2 + 3
```

The expression:

```lean id="i8w6x2"
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:

```lean id="yai1jk"
#eval Nat.add 2 3
#eval 2 + 3
```

Both evaluate to:

```text id="ctxwt2"
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`:

```lean id="gfcmc0"
#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.

```lean id="tve5tu"
#eval 2 + 3
#eval 10 - 4
#eval 3 * 5
```

Expected results:

```text id="zs8ljf"
5
6
15
```

Infix notation improves readability when the operation is naturally binary.

Common examples:

| Notation | Meaning        |
| -------- | -------------- |
| `x + y`  | addition       |
| `x * y`  | multiplication |
| `x = y`  | equality       |
| `P ∧ Q`  | conjunction    |
| `P ∨ Q`  | disjunction    |
| `P -> Q` | implication    |

## Precedence

Precedence controls grouping when parentheses are omitted.

```lean id="kbk4nt"
#eval 2 + 3 * 4
#eval (2 + 3) * 4
```

Expected results:

```text id="f4wlsh"
14
20
```

Multiplication binds more tightly than addition, so:

```lean id="hsie1k"
2 + 3 * 4
```

is parsed as:

```lean id="gzo7nq"
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:

```lean id="pe3vja"
#check 1 + 2 + 3
```

This is parsed as:

```lean id="3y2s6h"
(1 + 2) + 3
```

Many arithmetic operators associate to the left.

Function arrows associate to the right:

```lean id="jsfct2"
Nat -> Nat -> Nat
```

means:

```lean id="hpmkg0"
Nat -> (Nat -> Nat)
```

Function application associates to the left:

```lean id="2gndid"
f x y
```

means:

```lean id="ucut1d"
(f x) y
```

These conventions explain currying and partial application.

## Prefix and Postfix Notation

A prefix operator appears before its argument.

```lean id="givf05"
#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:

```lean id="zid3uq"
#check Not
#check ¬ True
```

The expression:

```lean id="73u9gp"
¬ P
```

means:

```lean id="d2na3f"
Not P
```

## Custom Infix Notation

You can define custom notation for a function.

```lean id="cfohzu"
def maxNat (x y : Nat) : Nat :=
  if x ≤ y then y else x

infixl:65 " ⊔ₙ " => maxNat
```

Use it:

```lean id="8e64dl"
#eval 3 ⊔ₙ 7
#eval 9 ⊔ₙ 4
```

Expected results:

```text id="ptlqfy"
7
9
```

The declaration:

```lean id="2y5dqu"
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:

| Form     | Meaning           |
| -------- | ----------------- |
| `infixl` | left associative  |
| `infixr` | right associative |
| `infix`  | non-associative   |

Left associative notation is suitable for arithmetic-like operations.

```lean id="2p95tw"
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.

```lean id="2xazjl"
def squareNat (n : Nat) : Nat :=
  n * n

prefix:80 "□ " => squareNat

#eval □ 5
```

Expected result:

```text id="fd2rg3"
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.

```lean id="3cgto6"
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.

```lean id="0ok302"
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:

```lean id="8adk75"
Myproj.join
```

Use namespace-aware names to avoid collisions.

## Notation in Propositions

Logical notation is central in theorem statements.

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

Here:

```lean id="vxh2cv"
P ∧ Q
```

is notation for conjunction, and:

```lean id="y97w70"
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.

```lean id="lthka8"
#check Nat × String
#check Nat -> String
#check List Nat
```

The product type:

```lean id="p5gj72"
Nat × String
```

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

The function type:

```lean id="yo012o"
Nat -> String
```

represents functions from natural numbers to strings.

## Parentheses as Documentation

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

Prefer:

```lean id="t33e1x"
(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:

```lean id="n7jcgq"
#check (2 + 3)
```

Second, expose relevant declarations:

```lean id="2pgz33"
#check HAdd.hAdd
#check Nat.add
```

Third, add type ascriptions:

```lean id="ys1h4k"
#check ((2 : Nat) + (3 : Nat))
#check ((2 : Int) + (3 : Int))
```

Fourth, add parentheses to force grouping:

```lean id="rfkscc"
#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.