Email Gateway (Aug 18 2022 at 20:31): Email Gateway (Aug 18 2022 at 20:31):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
the code generation tutorial gives a recommendation for that application
(search for »interpretation« there). There is also the theory
»Interpretation_with_Defs« in src/HOL/ex for a experimental workaround.
The discussion what interpretation could and should do with definitions
stemming from locales is still ongoing (also sporadically on the mailing
list), but I myself must reconsider the whole matter again first before
I enter the discussion again.
Cheers,
Florian
signature.asc
Email Gateway (Aug 18 2022 at 20:31):From: Lukas Bulwahn <bulwahn@in.tum.de>
In our ITP 2011 paper, Andreas and I suggest an alternative approach
that allows code generation from locale definitions more easily than the
recommendation in the code generation tutorial.
Lukas
Email Gateway (Aug 18 2022 at 20:31):From: Tobias Nipkow <nipkow@in.tum.de>
Am 17/07/2012 19:08, schrieb Florian Haftmann:
Hi Peter,
Currently, I am defining those constants by hand, after the
interpretation, which causes lots of boilerplate in my real applications
with more than a dozen of definitions.the code generation tutorial gives a recommendation for that application
(search for »interpretation« there). There is also the theory
»Interpretation_with_Defs« in src/HOL/ex for a experimental workaround.
Interpretation_with_Defs works well for me, I use it repeatedly in session IMP.
Tobias
The discussion what interpretation could and should do with definitions
stemming from locales is still ongoing (also sporadically on the mailing
list), but I myself must reconsider the whole matter again first before
I enter the discussion again.Cheers,
Florian
Last updated: Apr 20 2024 at 01:05 UTC