Re: [isabelle] export_code ... checking

Hi Christian,

On 09.12.2014 16:06, Christian Sternagel wrote:
> Dear code export experts,
> do I assume correctly that
>   export_code f1 ... fN checking
> can be used to "check" whether code generation "works" (at least to some
> extend) for constants f1 ... fN. If so, is it an unofficial feature that
> shouldn't be used in production code?

it is fine to use.  It does juts check whether the generated code
compiles.  Recently Andreas has devised other mechanisms to really check
what the code does.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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