On Wed, 5 Sep 2012, Lawrence Paulson wrote:
I'm only talking about cases where “show" must inevitably fail.
Fortunately, such situations are rare, but if they can easily be
detected, they should be. Larry
On 5 Sep 2012, at 14:20, Lars Noschinski <[email protected]> wrote:
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).
With the "case that must fail" we are getting back to the tendencies of
this thread:
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-May/002736.html
where I failed to explain basic observations how warnings and errors get a
slightly different meaning in the Prover IDE model.
Concerning fixes (and implicit type abstractions) you know my basic plan
already: highlight the situation in the source text in a way that tells
the user what is there, and the user can then see by himself if it is what
he had in mind or should have in mind.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
