[isabelle-dev] Should code_abort remove the corresponding code equations?
andreas.lochbihler at inf.ethz.ch
Tue Jul 9 15:58:07 CEST 2013
I have often run into this problem myself, too, especially in case of non-termination. I
would find it sensible that code_abort deletes the code equation.
On 09/07/13 15:28, Johannes Hölzl wrote:
> Hi *,
> code_abort does not remove the corresponding code equations
> (in Isabelle 19764bef2730)
> definition "test = True"
> code_abort test
> value [code] test -- "outputs True"
> definition [code del]: "test2 = True"
> code_abort test2
> value [code] test2 -- "raises 'test' exception"
> Should code_abort remove the code equation for test? Otherwise the
> resulting program might be non-terminating.
> - Johannes
More information about the isabelle-dev