Fix #7136: proper error when pattern definition has unsupported arguments

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 #7136: proper error when pattern definition has unsupported arguments #7138

Closed andreasabel closed 4 months ago

andreasabel commented 4 months ago

This adds checking pattern synonyms for the following unsupported attributes:

quantity
cohesion
lock
tactic
naming

We also add missing test cases for:

instance
relevance

Further, we tighten the type of pattern synonym arguments from Arg Name to WithHiding Name, reflecting the state of affairs better. (Still does not exclude Instance statically, but didn't want a new type just for that.)

Closes #7136.

andreasabel commented 4 months ago

New commits address CI failures.