blob: 28bd1c03f572b10848f14f7339fe4f7c9536497c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
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).
Check (eq_refl 0%int63 <: normfr_mantissa one = 0%int63).
Check (eq_refl (1 << 52)%int63 <: normfr_mantissa half = (1 << 52)%int63).
Check (eq_refl (1 << 52)%int63 <: normfr_mantissa (-half) = (1 << 52)%int63).
Check (eq_refl 0%int63 <: normfr_mantissa (-one) = 0%int63).
Check (eq_refl 0%int63 <: normfr_mantissa zero = 0%int63).
Check (eq_refl 0%int63 <: normfr_mantissa nan = 0%int63).
Check (eq_refl (3 << 51)%int63 <: normfr_mantissa three_quarters = (3 << 51)%int63).
Check (eq_refl 0%int63 <<: normfr_mantissa one = 0%int63).
Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa half = (1 << 52)%int63).
Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa (-half) = (1 << 52)%int63).
Check (eq_refl 0%int63 <<: normfr_mantissa (-one) = 0%int63).
Check (eq_refl 0%int63 <<: normfr_mantissa zero = 0%int63).
Check (eq_refl 0%int63 <<: normfr_mantissa nan = 0%int63).
Check (eq_refl (3 << 51)%int63 <<: normfr_mantissa three_quarters = (3 << 51)%int63).
|
