[Agda] Agda's syntax declaration

[Andrea Vezzosi]

Indeed the "syntax _==_ x y = x === y" example could be changed to
"syntax _>>=_ e₁ (λ x → e₂) = x ← e₁ , e₂" to highlight what the
problem is, as compared to bind above.


By the way, if you find more to add to the docs feel free to send pull
requests :) We might get rid of some of those stubs one day.

Cheers,
Andrea


On Sat, Nov 4, 2017 at 12:42 PM, Frederik Hanghøj Iversen
<fhi.1990 at gmail.com> wrote:
> 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.
>
> As for the documentation I think this example:
>
> syntax _==_ x y = x === y
>
>
> 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.
>
> 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.
>
> Also, it's a bit funny to me that so many readthedocs articles have the
> disclaimer "this is a stub" xD
>
> On Fri, Nov 3, 2017 at 4:58 PM, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:
>>
>> Hi Frederik,
>>
>> it seems like the only documentation was in the CHANGELOG, so I
>> collected it here:
>>
>>
>> https://github.com/agda/agda/blob/master/doc/user-manual/language/syntax-declarations.lagda.rst
>>
>>
>> it should soon appear at http://agda.readthedocs.io/ , I presume.
>>
>> About the list syntax, I was able to find this gist, not sure how well
>> it works in practice though.
>>
>> https://gist.github.com/bishboria/8568581
>>
>> Cheers,
>> Andrea
>>
>> On Fri, Nov 3, 2017 at 2:06 PM, Frederik Hanghøj Iversen
>> <fhi.1990 at gmail.com> wrote:
>> > I recently discovered Agda's syntax directive. And just now discovered
>> > that as a user I can define my own syntax directive.
>> >
>> > The thing I'm talking about is exemplified in agda-stdlib in
>> > Data.Product:
>> >
>> >     Σ-syntax : ∀ {a b} (A : Set a) → (A → Set b) → Set (a ⊔ b)
>> >     Σ-syntax = Σ
>> >
>> >     syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
>> >
>> > Unfortunately I cannot find any documentation on this directive. If
>> > anyone has a resource please let me know.
>> >
>> > I was also wondering if it would be possible to use this directive to
>> > define a syntactical construct for e.g. lists with arbitrary elements.
>> > That is, I'd like to be able to write a syntax declaration allowing me
>> > to write.
>> >
>> >     [0,1,2]
>> >
>> > in stead of
>> >
>> >     0 ∷ 1 ∷ 2 ∷ []
>> >
>> >
>> > Is this possible?
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
>
> --
> Regards
> Frederik Hanghøj Iversen