When trying to add a predecessor function, I encountered what appears to be a bug, which can be seen by uncommenting line 99 in parse.rs. Running 3 (func) (\l.l 0 0) gives the result (λz.((z (λy.(λx.(y (y (y x)))))) (λy.(λx.(y (y x)))))), which, when called with F (in a separate expression), gives the expected result of (λy.(λx.(y (y x)))) (2). However, running (3 (func) (\l.l 0 0)) F (all in one expression) results in (λs.(λz.z)) (0). These two results should be the same.
The problem seems to be in beta_reduce (removing eta_convert has no effect on the bug).
When trying to add a predecessor function, I encountered what appears to be a bug, which can be seen by uncommenting line 99 in parse.rs. Running
3 (func) (\l.l 0 0)gives the result(λz.((z (λy.(λx.(y (y (y x)))))) (λy.(λx.(y (y x)))))), which, when called withF(in a separate expression), gives the expected result of(λy.(λx.(y (y x))))(2). However, running(3 (func) (\l.l 0 0)) F(all in one expression) results in(λs.(λz.z))(0). These two results should be the same.The problem seems to be in
beta_reduce(removingeta_converthas no effect on the bug).