Re: [isabelle] Code generation for typedefs with an invariant

Hi all,

> This is documented in Ondra's PhD thesis (, Section 6.4) and in isar-ref (page 282 for the Isabelle2021 edition).
> IIRC, Ondra had also considered extending the code generator but decided against as it would significantly increase the trusted code base (which now would need to take map functions into account).

I can confirm this since I backed this decision.  Sorry for the late reply.


Attachment: OpenPGP_signature
Description: OpenPGP digital signature

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