Re: [isabelle] code_thms does not print (not implemented) consistently for constructors
- To: cl-isabelle-users at lists.cam.ac.uk, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Subject: Re: [isabelle] code_thms does not print (not implemented) consistently for constructors
- From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
- Date: Mon, 21 Aug 2017 19:26:56 +0200
- In-reply-to: <firstname.lastname@example.org>
- Organization: TU Munich
- References: <email@example.com> <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1
>> 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.
Description: OpenPGP digital signature
This archive was generated by a fusion of
Pipermail (Mailman edition) and