[Logiweb] double definition
mrmr at diku.dk
Fri Jul 1 12:30:41 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.
So what I did was saying:
"[ math in theory system prime s lemma mendelson proposition...
end math ]"
and doing it twice.
Anyhow, not remembering much about compiler theory I ask if it isn't
something that could be caught somewhere by the compiler. Is it possible
More information about the Logiweb