Commit ec99f208 by Guillaume Melquiond

Prove FLT_format_B2R.

parent 1a10273e
 ... @@ -196,6 +196,15 @@ apply canonic_canonic_mantissa. ... @@ -196,6 +196,15 @@ apply canonic_canonic_mantissa. now destruct (andb_prop _ _ Hx) as (H, _). now destruct (andb_prop _ _ Hx) as (H, _). Qed. Qed. Theorem FLT_format_B2R : forall x, FLT_format radix2 emin prec (B2R x). Proof. intros x. apply FLT_format_generic... apply generic_format_B2R. Qed. Theorem B2FF_inj : Theorem B2FF_inj : forall x y : binary_float, forall x y : binary_float, B2FF x = B2FF y -> B2FF x = B2FF y -> ... @@ -317,15 +326,12 @@ rewrite <- F2R_opp. ... @@ -317,15 +326,12 @@ rewrite <- F2R_opp. now case sx. now case sx. Qed. Qed. Theorem is_finite_Bopp: forall x, Theorem is_finite_Bopp: forall x, is_finite (Bopp x) = is_finite x. is_finite (Bopp x) = is_finite x. Proof. Proof. now intros [| | |]. now intros [| | |]. Qed. Qed. Theorem bounded_lt_emax : Theorem bounded_lt_emax : forall mx ex, forall mx ex, bounded mx ex = true -> bounded mx ex = 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