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

	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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