No, but those local let opens people were talking about recently can. Another option that I use sometimes is to make a local &quot;dummy&quot; 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">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</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>
&gt; On 2012-10-15 12:16, Serge D. Mechveliani wrote:<br>
&gt;&gt; what is the `syntax&#39; declaration?<br>
&gt;<br>
&gt; See &quot;Mixfix binders&quot; in<br>
&gt;<br>
&gt;   <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&#39;  help to abbreviate  `DTO.Carrier ord&#39;  to  `A&#39;<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>