<div dir="ltr">It's great that Agda now has syntax declarations!<div><br></div><div>I'm confused by the design. What is implemented is:<div><pre style="box-sizing:border-box;font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre;margin:0px;padding:12px;line-height:normal;display:block;overflow:auto;color:rgb(64,64,64);font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial"><span class="gmail-kr" style="box-sizing:border-box;font-weight:bold">infixr</span> <span class="gmail-mi" style="box-sizing:border-box;color:rgb(0,153,153)">40</span> bind
<span class="gmail-kr" style="box-sizing:border-box;font-weight:bold">syntax</span> bind e₁ <span class="gmail-o" style="box-sizing:border-box;font-weight:bold">(</span>λ x <span class="gmail-ow" style="box-sizing:border-box;font-weight:bold">→</span> e₂<span class="gmail-o" style="box-sizing:border-box;font-weight:bold">)</span> <span class="gmail-ow" style="box-sizing:border-box;font-weight:bold">=</span> x ← e₁ , e₂</pre><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">Whereas what I would have expected is:</span></div><div><pre style="font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial;box-sizing:border-box;font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;font-size:12px;white-space:pre;margin:0px;padding:12px;line-height:normal;display:block;overflow:auto;color:rgb(64,64,64);background-color:rgb(255,255,255)"><span class="gmail-kr" style="box-sizing:border-box;font-weight:bold">infixr</span> <span class="gmail-mi" style="box-sizing:border-box;color:rgb(0,153,153)">40</span> _←_,_<br><span class="gmail-kr" style="box-sizing:border-box;font-weight:bold">syntax</span> x ← e₁ , e₂ = bind e₁ <span class="gmail-o" style="box-sizing:border-box;font-weight:bold">(</span>λ x <span class="gmail-ow" style="box-sizing:border-box;font-weight:bold">→</span> e₂<span class="gmail-o" style="box-sizing:border-box;font-weight:bold">)</span></pre><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial"><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">Can someone please enlighten me as to the rationale behind the current design? Cheers, -- P</span></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial"><br class="gmail-Apple-interchange-newline"></div><div style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial"><br></div><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div></div></div>