[Agda] `syntax'

[Daniel Peebles]

No, but those local let opens people were talking about recently can.
Another option that I use sometimes is to make a local "dummy" module
parametrized by the DTO, open the DTO, and then define your record inside
it:

module Dummy {c l1 l2: Level} (ord : DTO c l1 l2) where
  open DTO ord
  record Merge1 (m : Carrier) (xs: List Carrier) (ys : List Carrier) : Set
where
    ...

open Dummy



On Mon, Oct 15, 2012 at 12:20 PM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> 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
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121015/30ce49e2/attachment.html