Re: [mizar] Re: strict

[Jesse Alama <alama@stanford.edu>]

Adam Naumowicz <adamn@math.uwb.edu.pl> writes:

> On Tue, 9 Jan 2007, Jesse Alama wrote:
>
>> It turns out that transposing RLVECT_1 and VECTSP_1 in the
>> constructors directive doesn't eliminate the *4.  Are there some other
>> "strict"'s that are being imported here that I don't know about?
>
> Sorting the notations directive reveals one more article which can be
> suspected in this case, i.e. GROUP_1.
>
> notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, MCART_1,
>       FUNCT_2, BINOP_1, ORDINAL2, FINSET_1, NUMBERS, XCMPLX_0, NAT_1, INT_1,
>       CARD_1, MCART_2, STRUCT_0, LATTICES, RLVECT_1, GROUP_1, VECTSP_1,
>       VECTSP_9;
>
> With this order the statement should eventually be accepted ;-)

Success!  That worked.  Thanks!

>
>> How did you find out that it was the order of RLVECT_1 and VECTSP_1
>> that might be the source of the problem?
>
> As Josef's written in his follow-up - one may use the XML
> representation to check the exact meaning of all used notions.

I'm afraid I still don't quite understand, but now that I have a
working environment, I'll try to break it again and look at the XML
representations so that I can discover how I might have come to know
that the order of my notations was the culprit.

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference