CODEWITHSUNDEEP
syntaxagda
Silvio Mayolo
Silvio Mayolo

Reputation: 70407

What are the rules for custom syntax declarations in Agda?

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

Answers (1)

Jesper
Jesper

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

Related Questions