Re: [isabelle] selector theorems for records WAS: simps_of_case has problems with records



Hi Andreas,

> Another application of the Ctr_Sugar/BNF machinery would be generating selector equations from a record specification or specifying a record via its selectors. Here is an example of what I have in mind:
â
> Johannes HÃlzl has changed the definition of the complex numbers to a codatatype to be able to use primcorec which does these conversions already internally. Is there already something similar for extensible records which I have missed?

No, there is nothing like that. I think the key would be to extend âprimcorecâ to work with arbitrary âctr_sugarâs that have selectors, by building a degenerate corecursor (term) from the case constant. This would be fairly easy. I might even have a student to work on this.

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.