Commit 1c43951a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Match implementation with signature.

parent dc85790e
...@@ -119,10 +119,10 @@ Qed. ...@@ -119,10 +119,10 @@ Qed.
Definition fromZ n := Float (ZtoM n) exponent_zero. Definition fromZ n := Float (ZtoM n) exponent_zero.
Lemma fromZ_correct : Lemma fromZ_correct :
forall n, FtoX (toF (fromZ n)) = Xreal (IZR n). forall n, toX (fromZ n) = Xreal (IZR n).
Proof. Proof.
intros. intros.
simpl. unfold toX. simpl.
generalize (mantissa_sign_correct (ZtoM n)). generalize (mantissa_sign_correct (ZtoM n)).
case_eq (mantissa_sign (ZtoM n)) ; intros ; rewrite ZtoM_correct in *. case_eq (mantissa_sign (ZtoM n)) ; intros ; rewrite ZtoM_correct in *.
rewrite H0. rewrite H0.
......
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