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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
