summaryrefslogtreecommitdiff
path: root/mips/prelude.sail
diff options
context:
space:
mode:
Diffstat (limited to 'mips/prelude.sail')
-rw-r--r--mips/prelude.sail8
1 files 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)