[isabelle-dev] Should code_abort remove the corresponding code equations?

[Andreas Lochbihler]

Hi Johannes,

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.

Andreas

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.
>
> Greetings,
>   - Johannes