Lexical Structure
Keywords
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.
Numerals
A positive numeral is a non-empty sequence of digits.
A negative numeral consists of symbol - followed by a non-empty sequence of digits.
Identifiers
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 |.
Examples:
- 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.
Comments
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.