Kaustuv Chaudhuri

In my mental model, this would be disallowed because `{pi x\ $(x = app M N -> false)}` reduces to `nabla n, {$(n = app M N -> false)}` which...

Just an addendum, the whole reason for this proposal is to avoid defining a `eq` and `neq` by hand. I should have said this earlier.

I've committed a quick fix but it has a performance impact. Not sure how measurable. Also it may break some existing proofs because the numbering is different in some corner...

This breaks too many existing proofs. More testing is needed.

That ctx definition should not have been allowed because in terms n1, n2 etc. are always parsed as constants, not bound variables. Thanks for the report.

Seems reasonable. Thanks for the suggestion. I'll take a crack at it RSN.

Thanks Todd. I took the liberty of turning your bullets into checkboxes. About the annotated directory, I am not sure if it makes sense to divide them up based on...

Yes, @thatdalemiller and I have been discussing how to add a little bit of literate programming support to Abella so that we can interleave documentation and code in a web-page....

Interesting. I'm going to give this FR a high priority for the next release, given how often rewriting seems to be cropping up.

Thanks for the report. Unfortunately Abella does not keep source positions in the AST currently. This has been on my list of things to add for a while. Let me...