On 05.09.2012 15:13, Lawrence Paulson wrote:
Fixing a variable that ought to be free is an error.
Highlighting is useful, but you have to be quite alert to notice it. I seldom
notice it except in really blatant situations, like the same variable
highlighted in two different ways. If the context is simply wrong, the
highlighting should be absolutely unmissable.
Indeed, a variable shadowed by mistake is quite hard to detect. But is
there a clear rule whether a variable "ought to be free"? Shadowing has
its legitimate use cases (e.g. I usually shadow the "n" in induction
proofs on the naturals).
-- Lars
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
