RE: [mizar] Question about environments

["James Smith" <james.smith@aleph-one.com>]

Adam,

>The 'Element of' modes are mostly remnants of "the old way of writing in
Mizar", and their use should be gradually 
>eliminated in most cases, so the lack of automatic equivalence won't be
that bad, afterall.
>
>> I wondered about these definitions at the time, but I'm pretty sure I 
>> understand their utility now. Presumably they would become redundant 
>> if the aforementioned equivalences were indeed set up?
>
>They surely will when a bigger part of MML is revised to use 'real number'
instead of 'Element of REAL' :-)

I clearly have much to learn!

>> Moving on, given that the answer to my original question was an 
>> unequivocal 'no', I've changed the offending definition from...
>>
>> definition
>>  let n be number;
>>  attr n is square means
>>   ex m being Nat st n = m^2;
>> ::>                        *103
>> end;
>
>If that is the only problem, you just need a reservation saying that
natural numbers are also real numbers, so that the 
>definition of ^2 can be matched - use XREAL_0 for that.

Great, that's a much better solution.

I'll press on.

Kind regards,

James