[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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and