Unused constant in stdlib/floating_point
In floating_point.SingleFull
module, constant min_single
is defined but it's unused
(The same is true of DoubleFull
module) .
I think that it should be the following:
module SingleFull
use export SingleFormat
constant min_single : real = 0x1p-149
clone export GenFloatSpecFull with
type t = single,
constant max = max_single,
constant max_representable_integer = max_int,
constant min = min_single, (* Added by me *)
lemma Bounded_real_no_overflow
end