Closed ywata closed 3 years ago
This looks like some good work!
I have yet to look at it in detail, however, I will point out that I have just merge #533. This, coincidentally, introduced an idris-tests2.el
as well. It would be great if you can rebase your branch off of master and address the issues. I expect, and want, that you will replace my idris-tests2.el
with your own!
If you can do the rebase, I will then have a look at the PR in a bit more detail to see in their is anything that needs commenting on.
Thanks for the contribution, it is very much appreciated!
Right, I didn't expect a new PR for this work. Sorry about that. Does this mean we can close this PR?
The intention of this commit is to add idris2 tests. That includes:
Consideration: I added test3 target for newly created test cases but it should be in test2. Originally, there were 5 test cases in idris-tests2.el failed. 4 of them were resolved by (*1) but it remains. It may because ProofSearch is missing but as I'm not sure, I left the test case as it is.