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



Hi all,

> This is documented in Ondra's PhD thesis (https://www21.in.tum.de/~kuncar/documents/kuncar-phdthesis.pdf, 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.

	Florian

Attachment: OpenPGP_signature
Description: OpenPGP digital signature



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