[Date Prev][Date Next] [Chronological] [Thread] [Top]

Internal Error:2503



 I  have downloaded  the 5.2.30 beta  into  my PC.
when I run "FM19.exe" in the disk7 of the 5.2.30beta,  errors ocuured.

I  think that in mizar system "means it ="  is  the same as
" equals". However, I found that they are not same in some
casees. For example,the following definition causes "Internal
Error:2503".
-------------------------
 definition
 let f be FinSeq-Location;
 func bubble-sort f -> Macro-Instruction equals
:def4:  ::def4
   a1:=len f ';'
       (a3:= intloc 0) ';'
       Times(a1,
          a2 :=len f ';'
          Times(a2,
               if<0(a3,a2,
                  a4:=a2 ';'
                  SubFrom(a4,intloc 0) ';'
                 (a5:=(f,a4))  ';'
                  (a6:=(f,a2)) ';'
                  if<0(a6,a5,swap(f,a4,a2),SCM+FSA-Stop),
                  SCM+FSA-Stop)
::>                          *2503
          )
       );
  correctness
  @proof
  end;
end;
----------------------------
if  I rewrite the above definition by "means  it =" , instead of
"equals",   the "Internal Error :2503" does not occur.


  Jingchao   Chen