[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] referring to unlabeled theorems
On Sat, 17 Feb 2007, Jesse Alama wrote:
I'm trying to use FVSUM_1:22 in a proof I'm working on, but I get
error *192 ("Inaccessible theorem") when doing so. The problem seems
to be that the twenty-second theorem of FVSUM_1 is not labeled as
such, even though the semantic presentation of FVSUM_1 does assign a
label to this theorem. How can I refer to this theorem?
This error usually indicates lack of required constructors. Have you tried
constr -f <your-article> FVSUM_1:22
?
If there are any missing constructors, they should be reported with this
command.
The labelling of theorems in articles isn't important - the numbering is
calculated internally when the article is exported to the library, and it
is reflected in abstracts for reference.
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/
======================================================================