[Agda] Agda's syntax declaration

[Andrea Vezzosi]

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