Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] setup_lifting without code gen


view this post on Zulip Email Gateway (Aug 22 2022 at 16:38):

From: Gerwin.Klein@data61.csiro.au
One for the lifting/transfer and code generator experts:

I have a type that I’d like to define as a datatype, because it produces a nice constructor, code, etc setup, but the datatype also happens to be easy to define as a typedef, which gives me lifting and transfer to another type. I’d like to have both (of course ;-)).

The type_definition theorem is easy to derive, but the command “setup_lifting” will overwrite the code generator setup from the datatype definition, which mostly makes quickcheck fail on this type (I haven’t investigated precisely when, but it at least complains about not knowing the constructors of the datatype any more).

Is there a way to tell setup_lifting not to touch the code generator? Or a not too annoying way to do the job of setup_lifting manually?

Cheers,
Gerwin


Last updated: Mar 29 2024 at 04:18 UTC