RE: Question about environments

Hi,

On Fri, 8 Jan 2010, James Smith wrote:

> thanks kindly for your replies. I've spent the day sifting through them and
> digging around the MML again. From a beginner's standpoint it does seem a
> shame that the attributes natural, real, complex, etc are not equivalent to
> Element of NAT, REAL, COMPLEX, etc without explicit reference.

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' :-)

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

Best,

Adam

=======================================================================
Dept. of Programming and Formal Methods  Fax: +48(85)7457662
Institute of Informatics                 Tel: +48(85)7457559 (office)
University of Bialystok                  E-mail: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland     http://math.uwb.edu.pl/~adamn/
=======================================================================