Re: [isabelle] Transfer rule for undefined



Hi Ondřej,

Thank you for your suggestion, it works like a charm.

On 06/06/13 14:35, Ondřej Kunčar wrote:
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.
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.

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?

Thanks again,
Andreas




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