search

agda / agda

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

Add `workOnTypes` reflection primitive #7310

Closed jespercockx closed 2 weeks ago

jespercockx commented 2 weeks ago

Somehow, the PR https://github.com/agda/agda/pull/6399 never got merged even though I could've sworn we had the workOnTypes primitive already. Since https://github.com/agda/agda/issues/6124 is not actually fixed without this feature, I am resurrecting this PR here.