data D : Set where x : D c : D → D pattern p x = c x test : D → D test (p x) = x
Reports at definition site of p:
Unused variable in pattern synonym
when scope checking the declaration
pattern p x = c x
Same problem when pattern variable shadows a pattern synonym rather than a constructor:
data D : Set where z : D c : D → D pattern x = z pattern p x = c x
A better error would inform me that I am trying to shadow a constructor (or pattern synonym) by a pattern variable, which does not work.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4