Re: [isabelle] Performing global rewrites on the code setup
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