# Language syntax

### Abstractions:
```
\x:T.e
```
Where `x` is an identifier, `T` a type, and `e` an expression

### Aplication:
```
lhs rhs
```
Where `lhs` and `rhs` are expressions

### Variable:
```
x
```
Where `x` is an identifier

### Constants:
```
n
```
where n is an number

or
```
true
```

or
```
false
```

## Types

The language has the primitive types `Bool` and `Nat`, and arrow types 
of the form `T1 -> T2`, where multiple of these can be composed, and 
parentesis can be used to specify associativity, ex: `(Nat -> Nat) -> Nat -> Nat`

# Using the repl

When entering a valid expression into the repl, it will be type checked, and if well typed,
its beta reduced form and type is printed.

The repl offers additional commands starting with `:`, the following commands are availaibe

- `:t expr`: get the type of `expr`, but do not beta reduce 
- `:ctx ident : T`: add a variable identfied by `ident` of type `T` to the type checking context,
arrow types need to be in parentesis