diff options
| -rw-r--r-- | kvx/FPDivision.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index ebf9136d..fad99f76 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -50,6 +50,8 @@ Proof. all: set (invb_d := (Float.of_single (ExtFloat32.inv (Float32.of_intu b)))). all: set (b_d := (Float.of_longu (Int64.repr (Int.unsigned b)))). all: cbn. + - admit. + - admit. Admitted. Definition approx_div a b := @@ -155,7 +157,7 @@ Proof. 2: lia. { unfold div_approx_reals. - fold a' b' prod_r. + fold a' b' prod' prod_r. unfold Int64.mul. rewrite Int64.unsigned_repr by admit. rewrite Int64.unsigned_repr by admit. |