Commit dbc1a5ed authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Allowed rewriting.

parent c1117205
......@@ -180,8 +180,7 @@ Theorem round_trunc_any_correct :
(0 <= x)%R ->
inbetween_float beta m e x l ->
(e <= fexp (digits beta m + e))%Z \/ l = loc_Exact ->
let '(m', e', l') := truncate (m, e, l) in
rounding beta fexp rnd x = F2R (Float beta (choice m' l') e').
rounding beta fexp rnd x = let '(m', e', l') := truncate (m, e, l) in F2R (Float beta (choice m' l') e').
Proof.
intros x m e l Hx Hl He.
generalize (truncate_correct x m e l Hx Hl He).
......
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