Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit dc3a4f5b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fixed exponent of square root.

parent 4114712a
......@@ -131,14 +131,14 @@ Definition Fsqrt_aux prec m e :=
let l :=
if Zeq_bool r 0 then loc_Exact
else loc_Inexact (if Zle_bool r q then Lt else Gt) in
(q, e'', l).
(q, Zdiv2 e'', l).
Theorem Fsqrt_aux_correct :
forall prec m e,
(0 < m)%Z ->
let '(m', e', l) := Fsqrt_aux prec m e in
(prec <= digits beta m')%Z /\
inbetween_float beta m' (Zdiv2 e') (sqrt (F2R (Float beta m e))) l.
inbetween_float beta m' e' (sqrt (F2R (Float beta m e))) l.
Proof.
intros prec m e Hm.
unfold Fsqrt_aux.
......
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