RE: 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
 
 <http://www.mygarble.com/> http://www.mygarble.com/