blob: a725deeeca7e79beccea61b8e36ceaf1689d7a2b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Require Import ZArith Int63 Floats.
Check (eq_refl : ldexp one 9223372036854773807%Z = infinity).
Check (eq_refl infinity <: ldexp one 9223372036854773807%Z = infinity).
Check (eq_refl infinity <<: ldexp one 9223372036854773807%Z = infinity).
Check (eq_refl : ldshiftexp one 9223372036854775807 = infinity).
Check (eq_refl infinity <: ldshiftexp one 9223372036854775807 = infinity).
Check (eq_refl infinity <<: ldshiftexp one 9223372036854775807 = infinity).
Check (eq_refl : ldexp one (-2102) = 0%float).
Check (eq_refl 0%float <: ldexp one (-2102) = 0%float).
Check (eq_refl 0%float <<: ldexp one (-2102) = 0%float).
Check (eq_refl : ldexp one (-3) = 0.125%float).
Check (eq_refl 0.125%float <: ldexp one (-3) = 0.125%float).
Check (eq_refl 0.125%float <<: ldexp one (-3) = 0.125%float).
Check (eq_refl : ldexp one 3 = 8%float).
Check (eq_refl 8%float <: ldexp one 3 = 8%float).
Check (eq_refl 8%float <<: ldexp one 3 = 8%float).
|
