Lexical Matters

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.