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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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