See the official user manual for the most up-to-date version of the information on this page.
Names
A name part is a non-empty sequence of printable Unicode characters not containing any of the following reserved characters.
@.(){};_
Furthermore, the following set of reserved words cannot be used as name parts.
-> : = ? \ | → ∀ λ abstract data forall hiding import in infix infixl infixr let module mutual open postulate primitive private public record renaming rewrite using where with Prop Set[0-9]* [0-9]+
This means
that strings like x:A
and A->B
are valid names. To write the
type signature and the function type, white space have to be inserted:
x : A
, and A -> B
.
A name is a non-empty sequence of alternating name parts and _
(excluding the singleton _
). A name containing _
can be used as an
operator where the arguments go in place of the _
. For instance, an
application of the name if_then_else_
to arguments x
, y
, and z
can
be written either as a normal application if_then_else_ x y z
or as
an operator application if x then y else z
.
A qualified name is a non-empty sequence of names separated by .
(dot). Qualified names are used to refer to entities in other modules.