See the official user manual for the most up-to-date version of the information on this page.
A name part is a string of printable characters not containing any of the following characters:
Furthermore, certain keywords may not be used as name parts.
A name is a sequence of one or more name parts separated by underscores (
A string like
a≤b (without spaces) is a valid name, and is different from
a ≤ b (with spaces). The latter actually refers to a type, whose terms are (roughly speaking) proofs that
a is less than or equal to
b. It is a standard convention to use a name like
a≤b for a variable of type
a ≤ b.
Similarly, strings like
A->B are names. To declare
x as a variable of type
A we must write
x : A (with spaces) rather than
x:A. To refer to the type of functions from
B, we must write
A -> B rather than
The meaning of underscores in names is explained in the section on mixfix operators. For example, the addition function is officially named
_+_ , and the placement of the underscores indicates that we can use the infix notation
a + b to refer to the value of the function at
A qualified name is a sequence of one or more unqualified names separated by dots (
Qualified names are used in naming modules and in referring to the contents of unopened modules.
For example, the proposition that a natural number
n is prime can be written in qualified form as
Data.Nat.Primality.Prime n, referring to a definition given in the standard library module
Data.Nat.Primality. The abbreviated notation
Prime n can be used after that module has
been imported and opened, as explained on the modules page.