Re: [isabelle] code del and code drop

>>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«.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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