Commit 097eb2a3 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Replace Z_of_nat' with Z_of_nat.

parent e035f878
......@@ -69,7 +69,7 @@ Definition bounded m e :=
Definition valid_binary x :=
match x with
| F754_finite _ m e => bounded m e
| F754_nan _ pl => (Z_of_nat' (S (digits2_Pnat pl)) <? prec)%Z
| F754_nan _ pl => (Z_of_nat (S (digits2_Pnat pl)) <? prec)%Z
| _ => true
end.
......@@ -77,7 +77,7 @@ Definition valid_binary x :=
Note that there is exactly one such object per FP datum.
NaNs do not have any payload. They cannot be distinguished. *)
Definition nan_pl := {pl | (Z_of_nat' (S (digits2_Pnat pl)) <? prec)%Z = true}.
Definition nan_pl := {pl | (Z_of_nat (S (digits2_Pnat pl)) <? prec)%Z = true}.
Inductive binary_float :=
| B754_zero : bool -> binary_float
......
......@@ -287,7 +287,7 @@ Local Open Scope Z_scope.
- apply J; omega.
- apply J; omega.
- destruct n as [pl pl_range]. apply Z.ltb_lt in pl_range.
apply J. apply D. unfold prec, Z_of_nat' in pl_range; omega. omega.
apply J. apply D. unfold prec in pl_range; omega. omega.
- unfold bounded in e0. apply Bool.andb_true_iff in e0; destruct e0 as [A B].
apply Z.leb_le in B.
unfold canonic_mantissa, FLT_exp in A. apply Zeq_bool_eq in A.
......
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