Currently pattern synonyms accept implicit arguments, but not instance arguments. One use case for this would be to make an argument that's not an instance argument available for instance search. For instance,
postulate
C : Set → Set
foo : {A : Set} {{i : C A}} → A
bar : {A : Set} → C A → A
bar i = foo -- fails since i is not eligible for instance search
pattern ! {{x}} = x
baz : {A : Set} → C A → A
baz ! = foo -- would work
An obstacle to the implementation is that pattern synonyms are expanded before we get to type checking and currently there's no way to represent in abstract syntax that a non-instance argument should nevertheless be available during instance search.
xekoukou, gallais, effectfully, solson, isovector and 1 more
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