[Agda] rewriting product types vs. single ctor data/record types
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.
> Agda mailing list
> Agda at lists.chalmers.se
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Agda