[Agda] `syntax'

[Serge D. Mechveliani]

Please, 
what is the `syntax' declaration?
(in Agda-2.3.0.1).
I see it in  Data.Product.agda.
In the  Agda reference manual  this keyword is highlighted in red.
Clicking at it does not showing the doc on `syntax', instead it asks
for "The password for editing normal pages is agda". 

Regards,
Sergei