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:<div>
<br></div><div>module Dummy {c l1 l2: Level} (ord : DTO c l1 l2) where</div><div> open DTO ord</div><div> record Merge1 (m : Carrier) (xs: List Carrier) (ys : List Carrier) : Set where</div><div> ...</div><div><br></div>
<div>open Dummy</div><div><br></div><div><br><div><br><div class="gmail_quote">On Mon, Oct 15, 2012 at 12:20 PM, Serge D. Mechveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On Mon, Oct 15, 2012 at 01:06:33PM +0200, Nils Anders Danielsson wrote:<br>
> On 2012-10-15 12:16, Serge D. Mechveliani wrote:<br>
>> what is the `syntax' declaration?<br>
><br>
> See "Mixfix binders" in<br>
><br>
> <a href="http://code.haskell.org/Agda/doc/release-notes/2-2-8.txt" target="_blank">http://code.haskell.org/Agda/doc/release-notes/2-2-8.txt</a>.<br>
<br>
<br>
</div>Can `syntax' help to abbreviate `DTO.Carrier ord' to `A'<br>
in the declaration<br>
<br>
record Merge1<br>
{c l1 l2 : Level} (ord : DTO c l1 l2)<br>
(m : DTO.Carrier ord) (xs : List $ DTO.Carrier ord)<br>
(ys : List $ DTO.Carrier ord) : Set ...<br>
where<br>
field list : List $ DTO.Carrier ord<br>
ordered : OrderedList? ord (m :: list)<br>
?<br>
<br>
Thanks,<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div></div>