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