Re: [isabelle] Code Generation: Error Messages



Hi Tjark,

> namely that they can be tedious to hunt down.  Getting
> 
>   *** No code equations for All
>   *** At command "export_code".
> 
> when trying to export code for some top-level constant that depends on
> All only through a lengthy chain of dependencies is helpful, but not
> really great.

there are a couple of diagnostic devices:

a) code_deps

b) code_thms

c) or even

	code_abort All
	export_code ...

But an explicit depedency trail would also make sense, and nowadays it
should be not that difficult to accomplish.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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.