Readme

README.md

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