Re: [isabelle] [ExternalEmail] setup_lifting without code gen



Answering my own question, there seems to be a somewhat distasteful hack that does make it work: use datatype_compat after lifting_setup. That looks like it does overwrite the code generator setup yet again.

If anyone has a better solution that doesn’t produce 3 code generator setups, I’d still be interested.

Cheers,
Gerwin

> On 24 Feb 2018, at 16:59, Gerwin.Klein at data61.csiro.au wrote:
> 
> 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



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