Re: [isabelle] Reflexive rewriting
On Mon, 13 Jul 2015, Manuel Eberl wrote:
I know how to fix this with NO_MATCH, but my question is this: why do we
not introduce a check in the simplifier that prevents it from rewriting
a term to itself? I don't know much about the simplifier, but I should
be surprised if such a check were difficult to implement, and I do not
think there would be a significant loss of performance. It also should
not break any existing proofs or code.
I am also not an expert on the Simplifier myself, but by default the blind
assumptions above need to be inverted. Just empirically, any tiny change
anywhere will cause lots of unexpected problems in obscure places.
This does not mean, reforms should not be done -- we do it all the time.
But it usually takes really long and hard work to push a change through.
This archive was generated by a fusion of
Pipermail (Mailman edition) and