search

agda / agda

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

#7245: warn about INJECTIVE_FOR_INFERENCE on non-functions #7275

Closed UlfNorell closed 2 weeks ago

UlfNorell commented 2 weeks ago

fixes #7245

and change other functions-only pragma errors to UselessPragma warnings