Email Gateway (Aug 19 2022 at 14:27): Email Gateway (Aug 19 2022 at 14:27):From: Tobias Nipkow <nipkow@in.tum.de>
I just spent more than half an hour trying to figure out where the problem with
my (long) poof was after I had discovered that the proposition was definitely
not true. Eventually I found a single sorry was left, attached to a wrong claim.
If sorry - which is definietly dangerous - had a dangerous colour, I would have
spotted it more quickly.
Tobias
Email Gateway (Aug 19 2022 at 14:27):From: Makarius <makarius@sketis.net>
In all official releases from 2013 there should be a "bad" markup for
sorry, after it was processed by the prover. That is neither an error nor
a warning (so it does not show up in the buffer overview column nor the
theories overview panel), but it has a thick red background and some
tooltip to tell the reason for the relative "badness".
If that special rendering was not to be seen, there might have been
something wrong elsewhere.
Makarius
Email Gateway (Aug 19 2022 at 14:27):From: Stephan van Staden <Stephan.vanStaden@inf.ethz.ch>
Is a "poof" a proof that is is almost complete but not quite right
because of a wrong detail? Or does it express that the proof suddenly
disappeared ("poof", and my "proof" was gone)?
If this is a neologism, which I suspect it is, then I must definitely
complement you on its originality :-)
Stephan
Email Gateway (Aug 19 2022 at 14:27):From: Tobias Nipkow <nipkow@in.tum.de>
Somehow my "Bad Color" had been changed to be invisible.
Thanks
Tobias
Last updated: May 06 2024 at 08:19 UTC