Re: [mizar] referring to unlabeled theorems

[Jesse Alama <alama@stanford.edu>]

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

> 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.

There indeed was a missing constructor (SETWOP_2) -- thanks for your
help!

> 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.

One thing that annoys me slightly is that the .miz form of a MIZAR
article doesn't necessarily have labels for all theorems.  I prefer to
look at MIZAR articles (not abstracts) in emacs, and sometimes I find
an unlabeled theorem that I want to use.  In these situations I have
to look at, e.g., the semantic presentation of that article or the
abstract to find out how to refer to that theorem.  It would be nice
if theorems in .miz files were labeled as they are in the abstracts
and the semantic presentation.

Thanks again,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*102: Unknown predicate (http://www.mizar.org)