Notation

v : τ means value v has type τ.
X = a means that a type or a value X is an alias for a.
X := [something] means that X is defined to be [something]
A percent sign % preceded only by spaces starts a line comment % [comment]
We use · to denote that we do not care about the value some variable takes. For example, when quantifying over a set of tuples of the form [math]\displaystyle{ (x, y) }[/math] we may use a [math]\displaystyle{ (x, \cdot) }[/math] to express that we do not care about the value [math]\displaystyle{ y }[/math] takes in each of the tuples.
Let [math]\displaystyle{ X }[/math] be a set or a sequence. We use [math]\displaystyle{ |X| }[/math] to denote the size/length of the set/sequence.