[ProofPower] Re: Type-check bug?

[Stephen Brackin]

After Roger Jones figured out that my problem came from type variables, I
started trying to solve it by taking the first course he suggested, namely
stating a more specific goal that explicitly mentions all the type
variables;  that's what worked for me in HOL90.  I went back to my Z theory,
intending to modify all my schema definitions so that every schema
explicitly names every type variable that it uses.  This gave me another
surprise, though, a "contains type variables not found in type of constants
to be defined" error.  After sanitizing and pruning, I got it down to the
following:

new_theory "test";
set_flag ("z_type_check_only", false);
%SZS% S1 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%
%BV% x1: TV1;
%BV% x2: %bbP% TV2
^
%SZS% S2 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%
%BV% x3: %bbP% S1
^
%SZS% S3 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%
%BV% x4: %bbP% S2

So how does one tell pp that S3 depends on TV1 and TV2 but on no other type
variables?

Steve
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lemma-one.com/pipermail/proofpower_lemma-one.com/attachments/20040920/f9964a0e/attachment.htm>