[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: strict
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 ;-)
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.
Best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================