Re: [isabelle] Performing global rewrites on the code setup
Function transformers are indeed only called on a single function at a time. Moreover,
they are not called at all on functions with abstract code equations (of the form Rep (f
x) = ...). They are mainly used to change the pattern-matching structure of functions.
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?
On 09/10/17 17:53, Lars Hupel wrote:
I am trying to apply a function "thm list -> thm list" to the global set
of code equations. I thought "functrans" allow me to do that, but
apparently they only work locally (i.e. on a single function). My use
case is to unfold all constants of arity zero.
This archive was generated by a fusion of
Pipermail (Mailman edition) and