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): http://isabelle.in.tum.de/repos/isabelle/file/43e07797269b/src/Pure/Isar/code.ML#l1253 http://isabelle.in.tum.de/repos/isabelle/file/43e07797269b/src/Pure/Isar/code.ML#l1275 Then the input syntax is adjusted accordingly using Pluing_Name.parse_filter, e.g. http://isabelle.in.tum.de/repos/isabelle/file/43e07797269b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML#l1081 Does this help? All the best, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
