[Date Prev][Date Next] [Chronological] [Thread] [Top]

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



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