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
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
Require Import ZArith Floats.
Definition two := Eval compute in (one + one)%float.
Definition half := Eval compute in (one / two)%float.
Definition huge := Eval compute in Z.ldexp one (1023)%Z.
Definition tiny := Eval compute in Z.ldexp one (-1022)%Z.
Definition denorm := Eval compute in Z.ldexp one (-1074)%Z.
Check (eq_refl : valid_binary (Prim2SF zero) = true).
Check (eq_refl : valid_binary (Prim2SF neg_zero) = true).
Check (eq_refl : valid_binary (Prim2SF one) = true).
Check (eq_refl : valid_binary (Prim2SF (-one)) = true).
Check (eq_refl : valid_binary (Prim2SF infinity) = true).
Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true).
Check (eq_refl : valid_binary (Prim2SF huge) = true).
Check (eq_refl : valid_binary (Prim2SF tiny) = true).
Check (eq_refl : valid_binary (Prim2SF denorm) = true).
Check (eq_refl : valid_binary (Prim2SF nan) = true).
Check (eq_refl : valid_binary (Prim2SF two) = true).
Check (eq_refl : valid_binary (Prim2SF half) = true).
Check (eq_refl true <: valid_binary (Prim2SF zero) = true).
Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true).
Check (eq_refl true <: valid_binary (Prim2SF one) = true).
Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true).
Check (eq_refl true <: valid_binary (Prim2SF infinity) = true).
Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true).
Check (eq_refl true <: valid_binary (Prim2SF huge) = true).
Check (eq_refl true <: valid_binary (Prim2SF tiny) = true).
Check (eq_refl true <: valid_binary (Prim2SF denorm) = true).
Check (eq_refl true <: valid_binary (Prim2SF nan) = true).
Check (eq_refl true <: valid_binary (Prim2SF two) = true).
Check (eq_refl true <: valid_binary (Prim2SF half) = true).
Check (eq_refl true <<: valid_binary (Prim2SF zero) = true).
Check (eq_refl true <<: valid_binary (Prim2SF neg_zero) = true).
Check (eq_refl true <<: valid_binary (Prim2SF one) = true).
Check (eq_refl true <<: valid_binary (Prim2SF (-one)) = true).
Check (eq_refl true <<: valid_binary (Prim2SF infinity) = true).
Check (eq_refl true <<: valid_binary (Prim2SF neg_infinity) = true).
Check (eq_refl true <<: valid_binary (Prim2SF huge) = true).
Check (eq_refl true <<: valid_binary (Prim2SF tiny) = true).
Check (eq_refl true <<: valid_binary (Prim2SF denorm) = true).
Check (eq_refl true <<: valid_binary (Prim2SF nan) = true).
Check (eq_refl true <<: valid_binary (Prim2SF two) = true).
Check (eq_refl true <<: valid_binary (Prim2SF half) = true).
|
