Re: [isabelle] code_thms does not print (not implemented) consistently for constructors



Hi Andreas,

>> IMO constructors declared with code_datatype should not be marked as
>> "not implemented" because I'd prefer if this is reserved for constants
>> that are actually missing code equations.

your observation actually triggered an inspection, substantially
reformulation and clarification of considerable parts of the code
generator data store which maybe will lead to some kind of localized
code generation in the future.

Now you may inspect whether the output of the diagnostic code generator
commands seems reasonable.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.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.