See the official user manual for the most up-to-date version of the information on this page.
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 ;
that strings like
A→B are valid names. To write the
type signature and the function type, white space has 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
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.