[mizar] puzzle

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hello,

I got quite puzzled for a while this morning when Mizar didn't want to
accept
     1*2=2;
but accepted
     2*1=2;
Requirements ARYTM was included in the environment, so such a trivial
equality should be obvious for the checker... I was just about to start
debugging the requirements implementation when I realized that it is due
to notation JORDAN2C :-)

definition let n;
   func 1*n -> FinSequence of REAL equals
:: JORDAN2C:def 7
   n |-> (1 qua Real);
end;

Another trap of the same kind is:

 definition let n;
   func 0*n -> FinSequence of REAL equals
:: EUCLID:def 4
   n |-> (0 qua Real);
 end;

As these are rather technical notions, maybe it would be better to replace
them by less ambiguous symbols ?

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================