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

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

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

I believe it is an old feature (not ver. 7). After widening of the type,
we do not round up the result.
I mean that if the type 'Element of REAL' is the result of widening,
then it gets only these adjective that were
in the widened type.
I am not certain, I have to check it. Because you do not want to correct
it, I do not write
how to fix it.

All the best,
Andrzej