Was asked today if #Agda has the equivalent of Coq's @ syntax to make arguments to a function explicit. Couldn't find anything so I wrote a small macro to do just that:
Conversation
Does this work even if the body of the implementation pattern matches on the implicit arguments? Or is that fixed in `unify goal u'`?
1
Ohhh wait, I see, the macro is wrapping the function with the implict argument in an explicit lambda. Nice!