blob: 6cc9f5ef924ad73c49d2682098910bd7c0557946 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Require Import Int63 ZArith Floats.
Definition half := ldexp one (-1)%Z.
Definition three_quarters := (half + (ldexp one (-2)%Z))%float.
Check (eq_refl : normfr_mantissa one = 0%int63).
Check (eq_refl : normfr_mantissa half = (1 << 52)%int63).
Check (eq_refl : normfr_mantissa (-half) = (1 << 52)%int63).
Check (eq_refl : normfr_mantissa (-one) = 0%int63).
Check (eq_refl : normfr_mantissa zero = 0%int63).
Check (eq_refl : normfr_mantissa nan = 0%int63).
Check (eq_refl : normfr_mantissa three_quarters = (3 << 51)%int63).
|
