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
|
Require Import ZArith Floats.
Definition epsilon := Eval compute in Z.ldexp one (-1024)%Z.
Check (eq_refl : classify one = PNormal).
Check (eq_refl : classify (- one)%float = NNormal).
Check (eq_refl : classify epsilon = PSubn).
Check (eq_refl : classify (- epsilon)%float = NSubn).
Check (eq_refl : classify zero = PZero).
Check (eq_refl : classify neg_zero = NZero).
Check (eq_refl : classify infinity = PInf).
Check (eq_refl : classify neg_infinity = NInf).
Check (eq_refl : classify nan = NaN).
Check (eq_refl PNormal <: classify one = PNormal).
Check (eq_refl NNormal <: classify (- one)%float = NNormal).
Check (eq_refl PSubn <: classify epsilon = PSubn).
Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn).
Check (eq_refl PZero <: classify zero = PZero).
Check (eq_refl NZero <: classify neg_zero = NZero).
Check (eq_refl PInf <: classify infinity = PInf).
Check (eq_refl NInf <: classify neg_infinity = NInf).
Check (eq_refl NaN <: classify nan = NaN).
Check (eq_refl PNormal <<: classify one = PNormal).
Check (eq_refl NNormal <<: classify (- one)%float = NNormal).
Check (eq_refl PSubn <<: classify epsilon = PSubn).
Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn).
Check (eq_refl PZero <<: classify zero = PZero).
Check (eq_refl NZero <<: classify neg_zero = NZero).
Check (eq_refl PInf <<: classify infinity = PInf).
Check (eq_refl NInf <<: classify neg_infinity = NInf).
Check (eq_refl NaN <<: classify nan = NaN).
|
