data C : Set where
c : C → C
pattern p {x = y} = c y
works : C → C
works (p {x}) = x
fails : C → C
fails (p {x = y}) = y
Bad arguments to pattern synonym
p
If I define the pattern synonym unnamed or de-facto unnamed way, the problem goes away:
pattern p {x} = c x
pattern p {x = x} = c x
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