[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