Re: [isabelle] Code equation for term_of_integer contains illegal numeral expression

Hi Andreas,

> I am not particularly familiar with all this term reconstruction stuff,
> but I found the following. In Code_Evaluation, there's a custom
> serialisation of term_of for integer for the target Eval. Narrowing,
> however, uses the target Haskell_Quickcheck, which is not a sub-target
> of Eval. Is there just an adaptation missing?

I interpret this as that the regular evaluation using »value [code] …«
etc. is operative but Quickcheck Narrowing breaks.  I follow your
analysis that a corresponding adaption for integer is missing for
Haskell_Quickcheck.  Never did I attempt to understand fully the rather
fancy and specialist adaption setup for Haskell_Quickcheck, but I guess
you easily find out what to add by experimenting with a setup for
term_of similar to that of Eval.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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