-
Notifications
You must be signed in to change notification settings - Fork 0
Open
Labels
Description
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).