Reputation: 70407
The Agda docs don't really have much to say on syntax
declarations, and a cursory glance at the source code is less than illuminating, so I've been trying to piece it together myself using examples from the standard library like Σ[_]_
and ∃[_]_
. I can reproduce an (admittedly rather contrived) example like theirs fairly easily
twice : {A : Set} → (A → A) → A → A
twice f x = f (f x)
syntax twice (λ x → body) = twice[ x ] body
But when I try to define custom syntax that binds two variables, I get an error
swap : {A B C : Set} → (A → B → C) → B → A → C
swap f y x = f x y
syntax swap (λ x y → body) = swap[ x , y ] body
Specifically,
Parse error
y<ERROR>
→ body) = swap[ x , y ] body
...
So I assume there are some rules as to what's allowed on the left-hand side of a syntax
declaration. What are these rules, and what of them prohibits my two-variable lambda form above?
Upvotes: 4
Views: 239
Reputation: 2965
Currently Agda does not allow syntax declarations with multi-argument lambda abstractions. This is a known limitation, see the issue tracker for the corresponding enhancement request.
Upvotes: 1