README.md

@@ -36,7 +36,7 @@ here is a list of the features (or better, limitations) I want to introduce:
 
 milly's full grammar is specified as a pair of lex and yacc files in `ref_parser/`.
 
-kakoune plugin for milly is in `kakoune_rc/milly.kak`.
+kakoune plugin for milly is in `extra/milly.kak`.
 
 Here is a small example of the syntax:
 

docs/operational_semantics.md

@@ -1,73 +0,0 @@
-# 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