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,
the
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: ]]

--
  Peter




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
> from
> Isabelle2017 does not contain any »code del«.
> 
> 	Florian
> 




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