Lexical Structure


All Arend’s keywords begin with \. Here’s the complete list of keywords:

\open \import \hiding \as \using \truncated \data \cons \func \lemma \axiom \sfunc \type \class \record \meta \classifying \noclassifying \strict \alias \field \property \override \default \extends \module \instance \use \coerce \level \levels \plevels \hlevels \box \eval \peval \with \elim \cowith \where \infix \infixl \infixr \fix \fixl \fixr \new \this \Pi \Sigma \lam \let \let! \have \have! \in \case \scase \return \lp \lh \suc \max \oo \Prop \Set \Type.


A positive numeral is a non-empty sequence of digits. A negative numeral consists of symbol - followed by a non-empty sequence of digits.


An identifier consists of a non-empty sequence of lower and upper case letters, digits, and characters from the list '~!@#$%^&*-+=<>?/|[]:_. Exceptions are sequences that begin with a digit or symbol ', numerals, and reserved names such as ->, =>, _, :, and |.


  • Valid identifiers: xxx, +, $^~]!005x, ::, ->x, x:Nat, -5b, -33+7, --xxx, f'.
  • Invalid identifiers: 5b, -33, =>, α.

Infix and postfix notation

A postfix notation is an identifier which follows `. An infix notation is an identifier surrounded by `. Both of these notations are described in Definitions.


Multi-line comments are enclosed in {- and -} and can be nested. Single-line comments consist of a sequence of symbols - of length at least 2 followed by a whitespace followed by an arbitrary text until the end of the line. To give an example, --, --------, -- foo, and ------- foobar are comments but --foo, foo--bar, and ------foobar are not.