Email Gateway (Aug 18 2022 at 10:21): Email Gateway (Aug 18 2022 at 10:21):From: Tom Ridge <tjr22@cam.ac.uk>
Dear All,
We are using Isabelle2005, trying to get codegeneration to work.
We have successfully extracted a simply typed lambda calc example. Now
we would like to extract something slightly bigger (defns attached).
Unfortunately it appears that mutually recursive datatypes are not
supported: the error when running stlc_codegen is
*** get_type_id: no such type: "stlc.t"
*** At command "code_module".
Can someone confirm this?
Thanks
Email Gateway (Aug 18 2022 at 10:22):From: Stefan Berghofer <berghofe@in.tum.de>
Tom Ridge wrote:
Dear Tom,
this is a bug that has already been fixed in the development
snapshot of Isabelle.
Greetings,
Stefan
Last updated: May 03 2024 at 08:18 UTC