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

Nils Anders Danielsson nad at cse.gu.se
Tue Aug 27 13:28:29 CEST 2013

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.


More information about the Agda mailing list