From 134f803b88a052996a1e20aa843e1ff6fe0f39a4 Mon Sep 17 00:00:00 2001
From: Avery <avery@gitea.itycodes.org>
Date: Thu, 13 Mar 2025 22:18:46 +0100
Subject: [PATCH] Readme

---
 README.md | 52 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 README.md

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..18f3806
--- /dev/null
+++ b/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