# Expressions

Every expression has a type that can be uniquely determined from the expression itself,
provided the expression is well-formed and well-typed.

```
Expression ::=
  | Literal
  | Id
  | OperatorExpr
  | FunctionCall
  | LabeledExpr
  | LetExpr
  | QuantifierExpr
  | "(" Expression ")"
```

## Literal expressions

```
Literal ::=
  | false | true
  | 0 | 1 | 2 | ...
  | "|" LiteralIdentifier ":" Type "|"
```

The literals `false` and `true` have the built-in type `bool`.

Natural numbers have the built-in type `int`. They are unbounded integers.

A _custom literal_ is an identifier-like token with a given type.
TODO: description

## Identifier expressions

```
Id ::=
  Identifier
```

The given identifier denotes a variable in scope, specifically

* in-, inout-, or out-parameter
* mutable or immutable local variable
* bound variable

## Operator expressions

```
OperatorExpr ::=
  | if Expression Expression else Expression
  | Expression BinaryOp Expression
  | UnaryOp Expression
BinaryOp ::=
  | "<==>"
  | "==>" | "<=="
  | "&&" | "||"
  | "==" | "!=" | "<" | "<=" | ">=" | ">"
  | "+" | "-"
  | "*" | "div" | "mod"
UnaryOp ::=
  | "!" | "-"
```

## Function calls

```
FunctionCall ::=
  Identifier "(" Expression*, ")"
```

TODO: description

## Labeled expressions

```
LabeledExpr ::=
  Identifier ":" Expression
```

The `Expression` parses as far as possible.

TODO: description

## Let expressions

```
LetExpr ::=
  val Identifier ":=" Expression Expression
```

Note that there is no punctuation between the two expressions.

TODO: description

## Quantifier expressions

```
QuantifierExpr ::=
  ( forall | exists ) Identifier ":" Type
  Pattern*
  Expression
Pattern ::=
  pattern Expression+,
```

TODO: description