Email Gateway (Aug 22 2022 at 16:38): Email Gateway (Aug 22 2022 at 16:38):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Gerwin,
AFAIK there's no way to prevent setup_lifting overwriting the code generator setup. (There
used to be a no_code option, but that's gone for a few releases.) However, datatype_compat
is a fairly heavyweight command to just fix the code generator setup. For example, this
command can change the default induction rules for mutually recursive datatypes. So
instead, I recommend to use
code_datatype <list of all constructors of the datatype>
right after the setup_lifting command. When you define constants with lift_definition, you
must derive your own code equations, though.
If this command does not suffice for quickcheck, you can restore the quickcheck setup with
quickcheck_generators <type name> constructors: <list of all constructors of the datatype>
Hope this helps,
Andreas
Email Gateway (Aug 22 2022 at 16:38):From: Gerwin.Klein@data61.csiro.au
Thanks, that is indeed a bit less hacky!
Cheers,
Gerwin
Last updated: Apr 16 2024 at 08:18 UTC