Email Gateway (Aug 22 2022 at 16:38): 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: Nov 21 2024 at 12:39 UTC