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

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.


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