[isabelle-dev] Proposal for localized interpretations
florian.haftmann at informatik.tu-muenchen.de
Wed Nov 26 15:59:17 CET 2014
Hi Andreas, hi Jasmin,
> It's quite nice as it is. Thanks!
> Andreas: I think I promised to help you with the code generator and "code_datatype" (cf. our private email conversation about "Quickcheck & Codatatypes"). I don't understand "code_datatype" (or what you do with it) well enough to do it without guidance, but if you are still interested please relaunch me on that, ideally after December 7.
In my understanding, this seems quite trivial. The first step is to
formally generalize the existing registration functions with
Plugin_Name.filter arguments (from data_default to data):
Then the input syntax is adjusted accordingly using
Does this help?
All the best,
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev