From b399242d6abfe0dced60396bb1abbea1156caafc Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 18 Jun 2018 17:39:24 +0100
Subject: Add bitvector length constraints to mips inequalities to match new
 constraints in prelude

---
 mips/prelude.sail | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/mips/prelude.sail b/mips/prelude.sail
index b2c2931b..f0ce2e5e 100644
--- a/mips/prelude.sail
+++ b/mips/prelude.sail
@@ -169,10 +169,10 @@ infix 4 >=_s
 infix 4 <_u
 infix 4 >=_u
 
-val operator <_s  : forall 'n. (bits('n), bits('n)) -> bool
-val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool
-val operator <_u  : forall 'n. (bits('n), bits('n)) -> bool
-val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool
+val operator <_s  : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator >=_s : forall 'n, 'n > 0. (bits('n), bits('n)) -> bool
+val operator <_u  : forall 'n, 'n >= 0. (bits('n), bits('n)) -> bool
+val operator >=_u : forall 'n, 'n >= 0. (bits('n), bits('n)) -> bool
 
 function operator <_s  (x, y) = signed(x) < signed(y)
 function operator >=_s (x, y) = signed(x) >= signed(y)
-- 
cgit v1.2.3