See the official user manual for the most up-to-date version of the information on this page.
The following keywords cannot be used as name parts:
= | -> : ? \ → ∀ λ abstract constructor data field forall hiding import in infix infixl infixr let module mutual open postulate primitive Prop private public quoteGoal quoteTerm quote record renaming rewrite Set[0-9]* syntax unquote using where with
The following keywords may be used as name parts:
The following characters are included here for indexing purposes: