Identifiers

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 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 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.