Commit 6ce2052c authored by MARCHE Claude's avatar MARCHE Claude

More on floats for model full

parent 5a715168
......@@ -180,7 +180,8 @@ Definition gt(x:floating_point.DoubleFormat.double)
(y:floating_point.DoubleFormat.double): Prop := ((value y) < (value x))%R.
(* Unused content named double
(* (* Unused content named double
exact (t 53 1024).
Defined.
*)
*)
......@@ -188,7 +188,8 @@ Definition gt(x:floating_point.SingleFormat.single)
(y:floating_point.SingleFormat.single): Prop := ((value y) < (value x))%R.
(* Unused content named single
(* (* Unused content named single
exact (t 24 128).
Defined.
*)
*)
......@@ -540,9 +540,7 @@ theory SingleFull
use export SingleFormat
constant max_single : real = 0x1.FFFFFEp127
constant min_single : real = 0x1p-149
constant max_int : int = 16777216 (* 2^24 *)
clone export GenFloatSpecFull with
type t = single,
......@@ -557,9 +555,7 @@ theory DoubleFull
use export DoubleFormat
constant max_double : real = 0x1.FFFFFFFFFFFFFp1023
constant min_double : real = 0x1p-1074
constant max_int : int = 9007199254740992 (* 2^53 *)
clone export GenFloatSpecFull with
type t = double,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment