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

Hi Lars,

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:
Dear list,

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 MHonArc.