[Agda] Syntax declarations

[Adam Sandberg Eriksson]

Ulf gave a rationale last year on this list: https://lists.chalmers.se/pipermail/agda/2017/009810.html

—Adam

> On 18 Mar 2018, at 13:22, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> 
> It's great that Agda now has syntax declarations!
> 
> I'm confused by the design. What is implemented is:
> infixr 40
>  bind
> 
> syntax 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/
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda