2. Notational Conventions

2.1. Rocq

1

The formal specification described here is written in the specification language of the Rocq theorem prover. The language is a total, pure-functional, dependently-typed language allowing for describing systems in rigorous detail including machine-checked proofs of various chosen properties.

2

Readers are not expected to be able to understand the bodies of the proof texts, and doing so is not in any case required. As long as one can understand the meaning of the propositions being expressed, it suffices to trust that the proofs are correct as they are all machine-checked whenever the specification is published.

3

The full sources of the entire specification are published at the end of this book.

2.2. Unicode

1

The specification makes reference to the Unicode character set which, at the time of writing, is at version 13.0.0. The specification often references specific Unicode characters, and does so using the standard notation U+NNNN, where N represents a hexadecimal digit. For example, U+03BB corresponds to the lowercase lambda symbol λ.

2.3. Sets

1

Where the specification refers to sets, it is referring to sets as defined in Zermelo-Fraenkel set theory.

2.3.2. ZFC

Notation	Description
e ∈ A	e is an element of the set A
e ∉ A	e is not an element of the set A
{ x₀, x₁, ... xₙ }	A set consisting of values from x₀ to xₙ
{ e ∈ A \| p(e) }	A set consisting of the elements of A for which the proposition p holds
\|A\|	The cardinality of the set A; a measure of the number of elements in A
∅	The empty set
𝔹	The booleans
ℕ	The natural numbers
ℝ	The real numbers
ℤ	The integers
[a, b]	A closed interval in a set (given separately or implicit from the types of a and b), from a to b, including a and b
(a, b]	A closed interval in a set (given separately or implicit from the types of a and b), from a to b, excluding a but including b
[a, b)	A closed interval in a set (given separately or implicit from the types of a and b), from a to b, including a but excluding b
(a, b)	A closed interval in a set (given separately or implicit from the types of a and b), from a to b, excluding a and b
A ⊂ B	A is a subset of, and is not equal to, B
A ⊆ B	A is a subset of, or is equal to, B
A ∩ B	The smallest set of elements that appear in both A and B (intersection).