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

Jason Gross jasongross9 at gmail.com
Tue Aug 27 17:34:51 CEST 2013

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

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

More information about the Agda mailing list