[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