[isabelle] setup_lifting without code gen

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?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.