Re: [isabelle] code del and code drop
I referred to pg 12 of the codegen tutorial (Isabelle2017 version):
"Normally, if constants without any code equations occur in a program,
code generator complains (since in most cases this is indeed an error).
[...] In order to categorise a constant into that category explicitly,
use the code
attribute with abort:"
However, if there are no code equations, the new behaviour is to handle
the constant as code-abort, and the behaviour mentioned in the first
sentence that I cited has to be forced with [[code drop: ]]
On So, 2018-05-06 at 17:12 +0200, Florian Haftmann wrote:
> > >
> > > From the NEWS file for 2017:
> > * Deleting the last code equations for a particular function using
> > [code del] results in function with no equations (runtime abort)
> > rather
> > than an unimplemented function (generation time abort). Use
> > explicit
> > [[code drop:]] to enforce the latter. Minor INCOMPATIBILITY.
> > Can please someone update the code generator tutorial Sec 2.5 (pg
> > 12).
> > I spent almost half an hour being puzzled why
> > definition [code del]: "foo == ..."
> > still admitted code generation for foo.
> What are you referring to exactly? The tutorial on code generation
> Isabelle2017 does not contain any »code del«.
This archive was generated by a fusion of
Pipermail (Mailman edition) and