[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
RE: [mizar] Question about environments
Good afternoon,
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. For example, I recalled that last week I saw
the following lines in REAL_1:
definition
let x be Real, y be real
number;
redefine func x+y -> Real;
coherence by
XREAL_0:def 1;
...
end;
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?
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;
...to...
definition
let n be number;
attr n is
square means
ex m being Element of NAT st n =
m^2;
end;
...which, although
different to that given in the tutorial, fixes the problem for now.
Many thanks again for all your
help.
Kind regards,
James