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

Fix #7176: turn absurd pattern in instance position to instance meta #7185

Closed andreasabel closed 3 months ago

andreasabel commented 3 months ago

Fix #7176: turn absurd pattern in instance position to instance meta rather than unification meta. So when we use a pattern synonym like pattern p = c {{()}} in an expression, the absurd pattern becomes an instance meta.