diff --git a/README.md b/README.md index f6935b6..8414fed 100644 --- a/README.md +++ b/README.md @@ -5,3 +5,29 @@ into a repl where you can type an expression in lambda calculus. Upon parsing this, you will be put into a new repl, where pressing enter will beta reduce the current term by one step. You can exit this by typing 'q' and pressing enter. I would recommend using `rlwrap`, as the repls are rather basic. + +Here's an example interaction showing each step of the beta reduction. +``` +> (lambda x y z. x z (y z)) (lambda x y. x) (lambda x y. x) +(λx y z. x z (y z)) (λx y. x) (λx y. x) +? +(λy z. (λx y. x) z (y z)) (λx y. x) +? +λz. (λx y. x) z ((λx y. x) z) +? +λz. (λy. z) (λy. z) +? +λz. z +? q +``` + +It will even handle name collisions and automatically alpha-rename. +``` +> (lambda x y. x y) (lambda x. y) +(λx y. x y) (λx. y) +? +λz. (λx. y) z +? +λz. y +? q +```