[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
RE: [mizar] 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: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
=======================================================================