mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
17 lines
537 B
Plaintext
17 lines
537 B
Plaintext
DoubleFormat: THEORY
|
|
BEGIN
|
|
% do not edit above this line
|
|
|
|
% Why3 double
|
|
double: TYPE+
|
|
|
|
% Why3 max_double
|
|
max_double: real =
|
|
(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)
|
|
|
|
% Why3 max_int
|
|
max_int: int = 9007199254740992
|
|
|
|
|
|
END DoubleFormat
|
|
|