-`t`). "`'a`" is a type variable (the tick mark just indicates that
-the variable ranges over types rather than values). "`τ1 -> τ2`" is
-the type of a function from expressions of type `τ1` to expressions of
-type `τ2`. And "`∀'a. τ`" is called a universal type, since it
-universally quantifies over the type variable `'a`.
-
-In the definition of the expressions, we have variables "`x`".
+`t`, or in arithmetic contexts, `N` or `Int`). "`'a`" is a type
+variable (the tick mark just indicates that the variable ranges over
+types rather than over values). "`τ1 -> τ2`" is the type of a
+function from expressions of type `τ1` to expressions of type `τ2`.
+And "`∀'a. τ`" is called a universal type, since it universally
+quantifies over the type variable `'a`. (You can expect that in
+`∀'a. τ`, the type `τ` will usually have at least one free occurrence
+of `'a` somewhere inside of it.)
+
+In the definition of the expressions, we have variables "`x`" as usual.