Remove redundant tests

SkySkimmer · Nov 24, 2023 · cd667e4 · cd667e4
1 parent 11c439b
commit cd667e4
Show file tree

Hide file tree

Showing 15 changed files with 174 additions and 959 deletions.
diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
@@ -11,23 +11,3 @@ 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).