Re: [isabelle] Transfer rule for undefined
Thank you for your suggestion, it works like a charm.
On 06/06/13 14:35, Ondřej Kunčar wrote:
This only applies to the development version, e.g., 608afd26a476. As is good practice on
isabelle-users, I have back-ported my problem to Isabelle2013 where there are only
non-parametric correspondence relations. But you rightly guessed that I am actually
working with the development version.
1) Quotient_my_int and Quotient_my_nat uses non-parametric correspondence relation
cr_my_int and cr_my_nat, whereas the transfer rules uses pcr_my_int and pcr_my_nat. In
this case you can just use my_int.pcr_cr_eq and my_nat.pcr_cr_eq to change the former
relations to the latter ones.
By the way, I wrap the type "32 word" in a type of its own to do the usual code generation
refinement stuff. When I call setup_lifting with the type definition, it warns that it
cannot generate a parametrized correspondence relation failed because it could not find a
relator for the type "Numeral_Type.bit0". Honestly, I have no clue what a relator for
these numeral types should look like. Or is it OK to ignore the warning in this case?
This archive was generated by a fusion of
Pipermail (Mailman edition) and