I have now a fairly complicated theory hierarchy
and its easy to mistakenly use a name which has already
been used somewhere.
I did this today and the resulting failure mode
seemed rather odd, so I wondered whether this is
how it is supposed to be or a sign of something amiss.
I defined the constant "Set" in a theory of miscellanea
("rbjmisc") high up in my hierarchy, forgetting that
this constant had already been used elsewhere.
It turned out that the previous use was in one of the
few theories which did not name rbjmisc as a parent,
so the second definition of Set went through OK, in
theory "nfu_f".
Then another theory is built which has both nfu_f and
rbjmisc as parents, causing a clash of names.
No complaint when the two parents are first nominated.
I just find that later one of my proofs fails.
When I rename the second version of Set, the proof
goes through OK.
In principle this might all be OK, since the two
definitions have disjoint types, but I didn't think
ProofPower allowed this kind of thing.
Is it supposed to be possible to get two definitions
of the same constant into scope in this way?
(or did I only have the wrong one in scope)
Roger Jones
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
