From f418e8617e627916d2dfa17e90b9994f6d445a61 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <34196198+Reijix@users.noreply.github.com>
Date: Mon, 17 Apr 2023 08:57:56 +0200
Subject: [PATCH] Create README.md

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

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..38e8353
--- /dev/null
+++ b/README.md
@@ -0,0 +1,38 @@
+# lambda
+This is a small lambda calculus interpreter.
+
+## Usage
+For best results you should run it using Nix, but using plain cabal should work in most cases as well!
+
+To run the interpreter just do
+```
+cabal run lambda
+```
+
+### Syntax
+A lambda calculus term can be one of:
+  - a variable
+  - application of two terms
+  - lambda abstracion
+
+This interpreter can handle lambda-terms and also supports declarations (assigning a name to a lambda-term).
+Following example should showcase all features:
+```
+> i = \x.x
+> s = \x.\y.\z.x z (y z)
+> k = \x.\y.x
+> s k k x
+s k k x
+(\x.\y.\z.x z (y z)) k k x
+(\v$0.\v$1.k v$1 (v$0 v$1)) k x
+(\v$0.k v$0 (k v$0)) x
+k x (k x)
+(\x.\y.x) x (k x)
+(\v$0.x) (k x)
+x
+```
+
+Behind the scenes the interpreter just exhaustively applies beta- and eta-reductions.
+
+### Prelude
+You can supply a prelude (a collection of functions that are loaded when the interpreter is started) to the interpreter in a file `prelude.lmd`.