# milly's semantics

We are going to define a desugared, restricted subset of `milly` called `core` for which we define an operational semantics.
Afterwards a translation from the full syntax to the `core` is defined.

## core

For now we ignore ground types and their terms.

Let us start by defining the `core` syntax:


```
t := t t                    (function application)
   | \x. t                  (lambda abstraction)
   | x                      (variable)
   | true                   (bool literal)
   | false                  (bool literal)
   | let v = t in t         (let expression)
   | (t_1, ..., t_n)        (tuple constructor)
   | #n t                   (tuple projection)
   | <alt: t>               (variant constructor)
   | match t                (case expression)
     {
       <alt_1: x_1> -> t_1
       ...
       <alt_n: x_n> -> t_n
     }
```

Values we consider:

```
v := \x. t           (Lambda function)
   | true            (bool value)
   | false           (bool value)
   | <alt: v>        (variant value)
   | (v_1, ..., v_n) (tuple value)
```

Types are:

```
type := bool                  (ground bool type)
      | type -> type          (function type)
      | <alt_1: type_1,       (variant type)
         ...,
         alt_n: type_n>
      | (type_1, ..., type_n) (product type)
```


Typing rules:

**Rule T-True**

> true : bool

**Rule T-False**

> false : bool

**Rule T-Tuple**

**If** t_1 : T_1, ..., t_n : T_n

> (t_1, ..., t_n) : (T_1, ..., T_n)

**Rule T-Proj**

**If** t : (T_1, ..., T_n)

> #k t : T_k