<div dir="ltr">This is really great. Thank you for putting this in the docs. I'll be sure to search the changelog next time I run into an undocumented feature.<div><br></div><div>As for the documentation I think this example:</div><div><br></div><div><pre style="box-sizing:border-box;font-family:SFMono-Regular,Consolas,"Liberation Mono",Menlo,Courier,monospace;font-size:13.6px;margin-top:0px;margin-bottom:0px;word-wrap:normal;padding:16px;overflow:auto;line-height:1.45;background-color:rgb(246,248,250);border-radius:3px;word-break:normal;color:rgb(36,41,46)">syntax _==_ x y <span class="gmail-pl-k" style="box-sizing:border-box;color:rgb(215,58,73)">=</span> x <span class="gmail-pl-k" style="box-sizing:border-box;color:rgb(215,58,73)">=</span>== y</pre></div><div class="gmail_extra"><br><div class="gmail_quote">Could benefit from a change. As far as I understand it the issue with this declaration is the LHS, i.e. _==_ and not the RHS ===, but I could be wrong. So perhaps it's a bit misleading.</div><div class="gmail_quote"><br></div><div class="gmail_quote">Maybe linking the gist for list-syntax would also be helpful (perhaps even adding it to agda-stdlib?) And the documentation could also expand on the caveat of using this approach as pointed out by NAD here and Toxaris in the Gist.</div><div class="gmail_quote"><br></div><div class="gmail_quote">Also, it's a bit funny to me that so many readthedocs articles have the disclaimer "this is a stub" xD</div><div class="gmail_quote"><br></div><div class="gmail_quote">On Fri, Nov 3, 2017 at 4:58 PM, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Frederik,<br>
<br>
it seems like the only documentation was in the CHANGELOG, so I<br>
collected it here:<br>
<br>
<a href="https://github.com/agda/agda/blob/master/doc/user-manual/language/syntax-declarations.lagda.rst" rel="noreferrer" target="_blank">https://github.com/agda/agda/<wbr>blob/master/doc/user-manual/<wbr>language/syntax-declarations.<wbr>lagda.rst</a><br>
<br>
<br>
it should soon appear at <a href="http://agda.readthedocs.io/" rel="noreferrer" target="_blank">http://agda.readthedocs.io/</a> , I presume.<br>
<br>
About the list syntax, I was able to find this gist, not sure how well<br>
it works in practice though.<br>
<br>
<a href="https://gist.github.com/bishboria/8568581" rel="noreferrer" target="_blank">https://gist.github.com/<wbr>bishboria/8568581</a><br>
<br>
Cheers,<br>
Andrea<br>
<div><div class="h5"><br>
On Fri, Nov 3, 2017 at 2:06 PM, Frederik Hanghøj Iversen<br>
<<a href="mailto:fhi.1990@gmail.com">fhi.1990@gmail.com</a>> wrote:<br>
> I recently discovered Agda's syntax directive. And just now discovered<br>
> that as a user I can define my own syntax directive.<br>
><br>
> The thing I'm talking about is exemplified in agda-stdlib in Data.Product:<br>
><br>
>     Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)<br>
>     Σ-syntax = Σ<br>
><br>
>     syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B<br>
><br>
> Unfortunately I cannot find any documentation on this directive. If<br>
> anyone has a resource please let me know.<br>
><br>
> I was also wondering if it would be possible to use this directive to<br>
> define a syntactical construct for e.g. lists with arbitrary elements.<br>
> That is, I'd like to be able to write a syntax declaration allowing me<br>
> to write.<br>
><br>
>     [0,1,2]<br>
><br>
> in stead of<br>
><br>
>     0 ∷ 1 ∷ 2 ∷ []<br>
><br>
><br>
> Is this possible?<br>
</div></div>> ______________________________<wbr>_________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div>Regards</div><div><i>Frederik Hanghøj Iversen</i></div></div>
</div></div>