Commit 8cef14ce authored by Guillaume Melquiond's avatar Guillaume Melquiond

Factored statement a bit.

parent b5e57af8
......@@ -954,9 +954,9 @@ Definition binary_round_sign_shl m sx mx ex :=
Theorem binary_round_sign_shl_correct :
forall m sx mx ex,
valid_binary (binary_round_sign_shl m sx mx ex) = true /\
let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in
let z := binary_round_sign_shl m sx mx ex in
valid_binary z = true /\
let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in
if Rlt_bool (Rabs (round radix2 fexp (round_mode m) x)) (bpow radix2 emax) then
FF2R radix2 z = round radix2 fexp (round_mode m) x /\
is_finite_FF z = true
......
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