[Agda] Syntax declarations

[Andreas Abel]

Phil, rest assured that you are not the only one stumbling over this 
design choice.

My explanation attempt:

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

can be read as

   print "bind e₁(λ x→  e₂)" as "x ← e₁ , e₂".

This reading emphasizes the uniqueness condition for syntax-attachments 
to a identifier ("bind").

And then, as a bonus, the parser can also handle "x ← e₁ , e₂" and treat 
it as "bind e₁(λ x→  e₂)".

Best,
Andreas

On 18.03.2018 14:22, Philip Wadler 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/


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/