Initial commit

test.lc

@@ -0,0 +1,14 @@
+-- id_0.lc
+let id   = \x -> x
+let zero = \f x -> x
+
+eval id_zero:
+  id zero
+  =d> (\x -> x) (\f x -> x)   -- expand definitions
+  =a> (\z -> z) (\f x -> x)   -- alpha rename
+  =b> (\f x -> x)             -- beta reduce
+  =d> zero                    -- expand definitions
+
+eval id_zero_tr:
+  id zero
+  =*> zero                    -- transitive reductions