mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
13 lines
257 B
Plaintext
13 lines
257 B
Plaintext
|
module ForLoop
|
||
|
|
use int.Int
|
||
|
|
use mach.java.lang.Integer
|
||
|
|
use mach.java.lang.Array
|
||
|
|
|
||
|
|
let all_equal_to (a : array integer) (x : integer) : bool =
|
||
|
|
for i = 0 to (length a - 1) do
|
||
|
|
if not (a[i] = x) then
|
||
|
|
return false;
|
||
|
|
done;
|
||
|
|
true
|
||
|
|
end
|