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 field codata constructor Prop Set[0-9]* [0-9]+ quote quoteGoal quoteTerm unquote syntax ;
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. See Mixfix for more information.
A qualified name is a non-empty sequence of names separated by .
(dot). Qualified names are used to refer to entities in other modules.