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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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