[isabelle-dev] Should code_abort remove the corresponding code equations?
andreas.lochbihler at inf.ethz.ch
Thu Jul 18 15:53:29 CEST 2013
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 exception code (instead of aborting).
I see, but I recommend that the attribute is not called [code del], but e.g. [code abort].
However, I am not sure whether I like this idea, because an attribute that acts on a
theorem seems weird, as "generate exception code" is a property of a constant rather than
a theorem. So I still think that something like
declare [[code_abort error_case_for_f]]
feels more natural than
declare some_thm_with_error_case_for_f_as_head_symbol [code_abort]
More information about the isabelle-dev