Notation

This page lists the notation Synthetic reads today: what each piece means, how a formula groups, which formulas read more than one way, and which readings can be sent to Lean. It covers the notation Synthetic starts with. Notation you declare in a Document isn’t read yet.

Each formula passes through up to four stages, and this page says how far each kind of formula goes:

Written: what you typed, which Synthetic keeps as you wrote it.
Read: the mathematical structures it recognizes in what you wrote. There may be more than one.
Sent to Lean: a reading Synthetic can write as a Lean statement, which Lean then checks.
Proved: not yet. A check leaves the statement’s proof as an obligation.

How to type each character, and which look-alike characters are read, is in the formula editor reference.

Constants

Written	Means
`𝒰`	the universe of types
`ℕ`	the natural numbers
`𝟎`	the empty type
`𝟏`	the unit type
`refl a`	the proof that `a = a`, also written `refl` with `a` in a subscript
0, 1, 2, …	natural numbers, written with the digits 0 to 9

Forms

In this table, A and B stand for any formula in the place they hold.

Written	Reads as
`A → B`, or `A -> B`	the type of functions from `A` to `B`
`(a : A) → B`	the type of functions taking each `a` in `A` to an element of `B`, which may mention `a`: the HoTT book’s Π
`A × B`, or `A * B`	the product of two types, or the product of two natural numbers
`(a : A) × B`	the type of pairs of an `a` in `A` and an element of `B`, which may mention `a`: the HoTT book’s Σ
`A + B`	the sum of two types, or the sum of two natural numbers
`a = b`	the type of equalities between `a` and `b`
`a = b`, with a type such as `ℕ` in a subscript on the `=`	the same, saying the type the equality is in
`A ≃ B`	equivalence of types
`f x`	`f` applied to `x`
`2 n`: a number before what it multiplies	2 times `n`
`n` with `2` in a superscript	`n` to the power 2, on natural numbers
`( … )`	what’s inside, read as one part

Superscripts and subscripts come from the editor’s toolbar, as the formula editor reference says. A name is any name a binder gives or the table above defines. Any other name, such as x in x + 1, is read, but it stands for nothing yet.

How a formula groups

Without parentheses, a formula groups by these, tightest first:

superscripts;
application, and a number before what it multiplies: f x y is (f x) y;
×;
+: a + b × c + d is (a + (b × c)) + d;
= and ≃: A × B = B × A is an equality between two products;
→ and the binders: x = y → P is a function out of an equality.

And within each:

→ groups to the right: A → B → C is A → (B → C).
+ and × group to the left: a + b + c is (a + b) + c.
= and ≃ don’t chain: a = b = c has no reading until it says which way it groups, as (a = b) = c or a = (b = c).
A binder, (a : A) → B or (a : A) × B, runs as far right as it can: its B takes the rest of the formula, as the HoTT book writes it.

Formulas that read more than one way

+ and × each mean two things: on types, a sum or a product; on natural numbers, addition or multiplication. Synthetic keeps every reading what they join allows, and leaves the choice to you.

A number settles it: n × 1 reads only as multiplication.
Names don’t: x + y reads two ways, and A × B = B × A four.
Synthetic doesn’t look at types when it reads, so n + m keeps its sum of types even where n and m are natural numbers. That reading can’t be sent to Lean, as the next section says.

To compare readings and choose one, see Readings and Lean checks.

Which readings can be sent to Lean

A check sends Lean a reading only where Synthetic can write it as a Lean statement. That takes all of these:

It is a statement. Equalities are, 𝟎 and 𝟏 are, and so are functions between statements, such as 𝟎 → 𝟏. Types of data aren’t: ℕ, ℕ → ℕ, ℕ × ℕ and ℕ + 𝟏 aren’t sent. Nor is a type of pairs such as (n : ℕ) × n = n, so “there is an n such that …”, written that way, isn’t sent.
Every name in it is bound or defined. x + y = y + x isn’t sent; (x : ℕ) → (y : ℕ) → x + y = y + x is, read with + as addition.
It stays among sets. A binder over the universe isn’t sent, as in (A : 𝒰) → A → A, and nor is 𝒰 itself, or an equality in a type not known to be a set.
Synthetic can write each part in Lean. It can’t yet write ≃.
Synthetic can work out each part’s type. Of the four readings of (n : ℕ) → (m : ℕ) → n + m = m + n, only the one where both + are addition is sent: a sum of types of two numbers has no type Synthetic can work out.
It isn’t too large for Synthetic to write.

Where a reading can’t be sent, the check says why, in the words of the rule it meets, such as “Lean checks statements; this reading isn’t one”.

What a check shows

Lean checks that the statement sent is one it can state, and leaves its proof as an obligation. So a false statement passes as readily as a true one: 0 = 1 and 1 + 1 = 3 are sent, as 1 + 1 = 2 is.

Two answers Lean 4 has given, as Synthetic’s tests record them:

(n : ℕ) → n + 0 = n: Lean checked the statement.
refl 0 = refl 1: Lean rejected it. Its two sides prove different equalities, 0 = 0 and 1 = 1, so no equality between them can be stated.

A check that Lean can state a reading isn’t a proof of it. Readings and Lean checks says what confirming a reading records.

Not read yet

notation declared in a Document;
logic’s own symbols, such as ∀, ∃, ¬, ∧ and ∨, and Π and Σ written as letters;
a minus sign, fractions and roots as arithmetic, and numbers other than the natural numbers, such as 2.5;
truncation.

This page describes Synthetic as it is now, and changes as notation is added.