Hi Florian,
On 18/07/13 15:07, Florian Haftmann wrote:
The idea is to have an explicit delete declaration, e.g. something like
definition error_case_for_f where [code del]: "error_case_for_f = f"
which will both have the effect of leaving no code equations for
error_case *and* generate excepti
Am 18.07.2013 12:28, schrieb Andreas Lochbihler:
> Hi Florian,
>
> On 18/07/13 12:00, Florian Haftmann wrote:
Should code_abort remove the code equation for test? Otherwise the
resulting program might be non-terminating.
>>>
>>> I have often run into this problem myself, too, especially
Hi Florian,
On 18/07/13 12:00, Florian Haftmann wrote:
Should code_abort remove the code equation for test? Otherwise the
resulting program might be non-terminating.
I have often run into this problem myself, too, especially in case of
non-termination. I would find it sensible that code_abort
>> Should code_abort remove the code equation for test? Otherwise the
>> resulting program might be non-terminating.
>
> 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.
Good equestion. G
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 Isab
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 cod
