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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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