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

Hi Andreas,

As unfolding should only be done on the right-hand sides of the
equations, I wonder why you don't just write a simproc that you add to
the preprocessor simpset?

I don't know all the constants and their code equations in advance. I literally want to unfold *all* constants with arity zero that are in the set of "code_thms" for a specific function. Otherwise I could just declare them as "[code_unfold]" when I define them.


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