[Logiweb] double definition

Martin Røpcke 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...
    peano all...
    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 
in pyk?


More information about the Logiweb mailing list