[Agda] Agda's syntax declaration

[Frederik Hanghøj Iversen]

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?