[Agda] rewriting product types vs. single ctor data/record types

[Jason Gross]

I think the feature being requested here might require anonymous record
types (or, possibly, automatic conversions between record types and sigma
types).

-Jason
On Aug 27, 2013 7:28 AM, "Nils Anders Danielsson" <nad at cse.gu.se> wrote:

> On 2013-08-25 19:45, Jonathan Leivent wrote:
>
>> Is there some way to rewrite "into" the fields of a data/record type
>> that appears as a goal, to achieve the same effect as rewriting would
>> on a very similar product type?
>>
>
> If you change the fields' types, then you may end up with something that
> is no longer an instance of the record type.
>
> --
> /NAD
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130827/89c9026f/attachment.html