[Agda] Syntax declarations

[Philip Wadler]

It's great that Agda now has syntax declarations!

I'm confused by the design. What is implemented is:

infixr 40 bindsyntax bind e₁ (λ x → e₂) = x ← e₁ , e₂

Whereas what I would have expected is:

infixr 40 _←_,_
syntax x ← e₁ , e₂ = bind e₁ (λ x → e₂)

Can someone please enlighten me as to the rationale behind the current
design? Cheers, -- P


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180318/1cd60090/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180318/1cd60090/attachment.ksh>