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



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.

Cheers
Lars




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