# Lexical Structure

## Keywords

All Arend’s *keywords* begin with `\`

.
Here’s the complete list of keywords:

\open \import \hiding \as \using \truncated \data \func \lemma \sfunc \class \record \field \property \extends \module \instance \use \coerce \level \eval \peval \with \elim \cowith \where \infix \infixl \infixr \fix \fixl \fixr \new \this \Pi \Sigma \lam \let \let! \in \case \scase \return \lp \lh \suc \max \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`

. - Invalid identifiers:
`5b`

,`-33`

,`=>`

.

## Infix and postfix notation

A *postfix notation* is an identifier followed by ```

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