search

agda / agda

Agda is a dependently typed programming language / interactive theorem prover.
https://wiki.portal.chalmers.se/agda/pmwiki.php
Other
2.48k stars 345 forks source link

[ #6406 ] Add test cases from discussion on this issue #7311

Closed jespercockx closed 3 months ago

jespercockx commented 3 months ago

I am looking again at issue #6406, and it seem that with the version of https://github.com/agda/agda/pull/6405 that got merged, the subject reduction problems discussed in that issue are no longer present. So I propose we add these tests and close the issue.

jespercockx commented 3 months ago

Merging this now, feel free to comment if there is still remaining problems.