[Logiweb] double definition
Klaus Ebbe Grue
grue at diku.dk
Fri Jul 1 12:49:32 CEST 2005
> I finally found an annoying error making things appear strange. I had defined
> a lemma twice, that is, using the same name two places. The error occured due
> to "copy-paste laziness" and now I have been taught a lesson. And besides,
> searching for the error made my proof a bit more simpel.
I suppose this is a follow up on [Logiweb] lemma proof mismatch.
If the pyk compiler sees that the same aspect of the same construct is
defined more than once, it compares the right hand sides of the
definitions and, if they differ, print a warning.
In particular, if a lemma is stated twice, the compiler prints a warning
unless the two instances are completely identical.
But the warning hides in the horrible amounts of output from the compiler.
Some day I think I choke the output from TeX. That should reduce the
amount of output to a level where it makes sense to spot warnings (but one
will risk to miss TeX warnings, of course).
More information about the Logiweb