Re: [isabelle] Code generation for typedefs with an invariant
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Code generation for typedefs with an invariant
- From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
- Date: Fri, 12 Nov 2021 19:35:49 +0100
- Authentication-results: cam.ac.uk; iprev=pass (mail-out1.in.tum.de) smtp.remote-ip=126.96.36.199; spf=pass smtp.mailfrom=informatik.tu-muenchen.de; arc=none
- In-reply-to: <D52B3CA3-E621-4918-B399-26B3223CDCD6@di.ku.dk>
- References: <email@example.com> <firstname.lastname@example.org> <email@example.com> <D52B3CA3-E621-4918-B399-26B3223CDCD6@di.ku.dk>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.13.0
> 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.
Description: OpenPGP digital signature
This archive was generated by a fusion of
Pipermail (Mailman edition) and