The tool does not recognize `λn. n` as eta-equivalent to the Church 1 (`λfn. f n`).

[anton-trunov]

This might prevent it from recognizing E := λmn. n m as a solution to the exponentiation problem. (I can't check it right now). But it certainly does not help when testing.

[evinism]

Thank you so much for contributing! I guess I'd love to know a little more about the theory here-- do we generally consider eta equivalence rather than just alpha equivalence when asking "is this church numeral 1?"

[anton-trunov]

Most sources seem to do so. E.g. when converting from a Church numeral to, say, integer one usually passes a (+1) function as the first argument and 0 as the second -- λfz. f z gets converted to 1, so does λx. x.

[evinism]

Solid, I'll implement that then(or you can if you want)!
some links for reference would be good, too, if you're willing.

[anton-trunov]

Off the top of my head: Wikipedia and "Types and Programming Languages" by B. Pierce assume eta-equivalence.

[evinism]

implemented in #51, still waiting on getting the book so i actually know what i'm doing

[anton-trunov]

Cool! Will try the tool again in some time! Thanks!