<p>I think the feature being requested here might require anonymous record types (or, possibly, automatic conversions between record types and sigma types).</p>
<p>-Jason</p>
<div class="gmail_quote">On Aug 27, 2013 7:28 AM, "Nils Anders Danielsson" <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
On 2013-08-25 19:45, Jonathan Leivent wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is there some way to rewrite "into" the fields of a data/record type<br>
that appears as a goal, to achieve the same effect as rewriting would<br>
on a very similar product type?<br>
</blockquote>
<br>
If you change the fields' types, then you may end up with something that<br>
is no longer an instance of the record type.<br>
<br>
-- <br>
/NAD<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div>