[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Re: strict
On Tue, 9 Jan 2007, Jesse Alama wrote:
The error definitely lies with the theorem, not with the summaries of
the error messages at the bottom of the file:
theorem
F2 is strict;
::> *4
Yes, it couldn't be that easy ;-)
Here's my environment; it's nasty:
vocabularies FINSET_1, POLYFORM, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1,
SUBSET_1, TARSKI, BOOLE, MCART_1, RELAT_1, NAT_1, XCMPLX_0, ORDINAL2,
VECTSP_1, VECTSP_9, INT_1, BINOP_1, MCART_2, RLVECT_1, GROUP_1;
notations FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, CARD_1,
SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, XCMPLX_0, ORDINAL2,
VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1, LATTICES, MCART_2,
RLVECT_1, GROUP_1;
constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1,
ZFMISC_1, SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL2,
VECTSP_1, VECTSP_9, INT_1, STRUCT_0, BINOP_1, LATTICES, MCART_2,
FRAENKEL, ENUMSET1, RLVECT_1, GROUP_1;
registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1,
SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0;
requirements NUMERALS, BOOLE, ARITHM, SUBSET;
definitions XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, MCART_2,
ENUMSET1, RLVECT_1, BINOP_1, STRUCT_0, GROUP_1; theorems XBOOLE_0,
FUNCT_1, RELAT_1, XBOOLE_1, TARSKI, ZFMISC_1, MCART_1, SUBSET_1,
FUNCT_2, MCART_2, ENUMSET1, BINOP_1, STRUCT_0, GROUP_1; schemes FUNCT_1,
BINOP_1;
Could it be that something in my environment is messed up?
Exactly - the offending part are the notations imported from RLVECT_1
after VECTSP_1 - this way your "strict" is the one automagically defined
for LoopStr instead for doubleLoopStr! The order of imported notations is
relevant, and it's best to use the 'mml.lar' list to control it - please
see the thread at:
http://mizar.uwb.edu.pl/forum/archive/0609/msg00071.html
If your work dosn't depend on this unfortunate transposition, you should
be able to just change the order of these two directives without any other
changes to your article and get rid of the *4.
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/
======================================================================