Re: [isabelle] Simplifier: renamed bound variable ":000" to ":000a"
On Wed, 17 Feb 2010, Brian Huffman wrote:
If I understand you correctly, the "renamed bound variable" message
indicates a problem in the *implementation* of some part of the
simplifier. So the message is only potentially useful to developers, and
not ordinary users.
No, it indicates that the Simplifier has just repaired a problem
introduced in user space, notably one of these Simplifier plugins that can
be defined in the library. Since the main library in question is actually
main HOL, one could nonetheless argue that it is somehow relevant to
I would like Isabelle to refrain from printing warning messages unless
they provide meaningful information that users can act upon.
I am usually trying hard to keep messages relevant, and fight spam
wherever possible, although this often seems futile. As messages are
cleaned up here, new ones emerge there.
Concerning this particular message, I would not just switch it of because
it is an important reminder that certain things in HOL still need to be
sorted out. Maybe you can help looking through all the simprocs ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and