From 1b0bd3a9e3a913a4928b68546a134a1a4448f9e8 Mon Sep 17 00:00:00 2001
From: Guillaume Bertholon
Date: Mon, 16 Jul 2018 13:30:37 +0200
Subject: Add tests for primitive floats

Add utility ldexp and frexp functions to prevent dealing with the shift of
ldshiftexp and frshiftexp everywhere.

Also move primitive integer tests to place all primitive tests in the
same directory.
---
 test-suite/arithmetic/unsigned.v | 18 ------------------
 1 file changed, 18 deletions(-)
 delete mode 100644 test-suite/arithmetic/unsigned.v

(limited to 'test-suite/arithmetic/unsigned.v')

diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/arithmetic/unsigned.v
deleted file mode 100644
index 82920bd201..0000000000
--- a/test-suite/arithmetic/unsigned.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(* This file checks that operations over int63 are unsigned. *)
-Require Import Int63.
-
-Open Scope int63_scope.
-
-(* (0-1) must be the maximum integer value and not negative 1 *)
-
-Check (eq_refl : 1/(0-1) = 0).
-Check (eq_refl 0 <: 1/(0-1) = 0).
-Check (eq_refl 0 <<: 1/(0-1) = 0).
-Definition compute1 := Eval compute in 1/(0-1).
-Check (eq_refl compute1 : 0 = 0).
-
-Check (eq_refl : 3 \% (0-1) = 3).
-Check (eq_refl 3 <: 3 \% (0-1) = 3).
-Check (eq_refl 3 <<: 3 \% (0-1) = 3).
-Definition compute2 := Eval compute in 3 \% (0-1).
-Check (eq_refl compute2 : 3 = 3).
-- 
cgit v1.2.3