Re: [isabelle] Performing global rewrites on the code setup

Hi Lars,

Am 10.10.2017 um 08:19 schrieb Lars Hupel:
>> Yes, I got that. That's why I suggested a simproc. The simproc should
>> be called on all
>> atoms of a term. If the atom is a constant, then it can get the code
>> equations for the constant and look whether it does not take any
>> argument. If so, use the code equation to generate the unfolding
>> theorem.
>> You can get the code equations for a specific constant from the
>> context by
>> Â Code.get_cert @{context} [] @{const_name map} |>
>> Code.equations_of_cert @{theory}
> Could this could be problematic because of potential loops where
> something in the preprocessor of the code will invoke the preprocessor
> again to obtain code equations? In any case, I'll try it out and let you
> know.

Code.get_cert @{context} [] does not involve any preprocessing.

What you are definitely loosing is the case that functions transformers
would reduce the number of arguments to 0.

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.