<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 3.2//EN">
<HTML>
<HEAD>
<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=us-ascii">
<META NAME="Generator" CONTENT="MS Exchange Server version 5.5.2657.73">
<TITLE>Re: Type-check bug?</TITLE>
</HEAD>
<BODY>
<P><FONT SIZE=2>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:</FONT></P>
<P><FONT SIZE=2>new_theory "test";</FONT>
<BR><FONT SIZE=2>set_flag ("z_type_check_only", false);</FONT>
<BR><FONT SIZE=2>%SZS% S1 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%</FONT>
<BR><FONT SIZE=2>%BV% x1: TV1;</FONT>
<BR><FONT SIZE=2>%BV% x2: %bbP% TV2</FONT>
<BR><FONT SIZE=2>^</FONT>
<BR><FONT SIZE=2>%SZS% S2 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%</FONT>
<BR><FONT SIZE=2>%BV% x3: %bbP% S1</FONT>
<BR><FONT SIZE=2>^</FONT>
<BR><FONT SIZE=2>%SZS% S3 [TV1, TV2] %BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%%BH%</FONT>
<BR><FONT SIZE=2>%BV% x4: %bbP% S2</FONT>
</P>
<P><FONT SIZE=2>So how does one tell pp that S3 depends on TV1 and TV2 but on no other type variables?</FONT>
</P>
<P><FONT SIZE=2>Steve</FONT>
</P>
</BODY>
</HTML>