Re: [mizar] Why doesn't this behave like I expect?

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

You need clusters from ARYTM_3.

More frustrating is the Nat vs natural number issue.

On Tue, Feb 10, 2004 at 08:09:16PM +0100, Freek Wiedijk wrote:
> Dear Mizar community,
> 
> I'm trying to prepare for my Mizar course, and now I don't
> understand something.  My excuses is this happens to be trivial.
> 
> Consider the following article:
> 
>   environ
>    vocabulary ARYTM;
>    notation XREAL_0, XCMPLX_0, NAT_1, SUBSET_1, NUMBERS, ORDINAL1;
>    constructors XREAL_0, XCMPLX_0, NUMBERS;
>    clusters XREAL_0, REAL_1;
>   begin
>    for x being Nat holds (x qua Element of REAL) is set;
>    for x being Element of REAL holds (x qua real number) is set;
>    for x being Nat holds (x qua real number) is set;
> ::>                           *116
> ::> 116: Invalid "qua"
> 
> So every Nat is an Element of REAL, and (because of the
> cluster in REAL_1, I hope) every Element of REAL has
> attribute "real".
> 
> My question: why does the Nat from the third line doesn't get
> the attribute "real" as well?
> 
> Please enlighten me :-)  I don't want to know how to fix this
> (how to get rid of that error), I want to know why this happens.
> 
> Freek
> (Ah, by the way, this is using Mizar 7.0.01.)
> ## RF mark: EXCEPTION: 'freek@cs.kun.nl'
> ## RF rules: ExcHF OK

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr