Commit c2313fc2 authored by MARCHE Claude's avatar MARCHE Claude

add missing definitional axiom for round_logic

parent 5bb78bd4
......@@ -92,7 +92,6 @@ theory GenFloat
type t
function round mode real : real
function round_logic mode real : t
function value t : real
function exact t : real
......@@ -138,6 +137,13 @@ theory GenFloat
axiom Round_up_neg:
forall x:real. round Up (-x) = - round Down x
(** rounding into a float instead of a real *)
function round_logic mode real : t
axiom Round_logic_def:
forall m:mode, x:real.
no_overflow m x ->
value (round_logic m x) = round m x
end
......
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