[Agda] `syntax'

[Serge D. Mechveliani]

On Mon, Oct 15, 2012 at 01:06:33PM +0200, Nils Anders Danielsson wrote:
> On 2012-10-15 12:16, Serge D. Mechveliani wrote:
>> what is the `syntax' declaration?
>
> See "Mixfix binders" in
>
>   http://code.haskell.org/Agda/doc/release-notes/2-2-8.txt.


Can  `syntax'  help to abbreviate  `DTO.Carrier ord'  to  `A'  
in the declaration

  record Merge1 
         {c l1 l2 : Level} (ord : DTO c l1 l2)  
         (m : DTO.Carrier ord) (xs : List $ DTO.Carrier ord) 
         (ys : List $ DTO.Carrier ord) : Set ...
       where 
       field list    : List $ DTO.Carrier ord   
             ordered : OrderedList? ord (m :: list)
?

Thanks,
Sergei