summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp_lib.lem4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 513e1b78..c58e9351 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -10,14 +10,14 @@ open import Bool
let hardware_mod (a: integer) (b:integer) : integer =
if a < 0 && b < 0
then (abs a) mod (abs b)
- else if (a < 0 && b >= 0) || (a >= 0 && b < 0)
+ else if (a < 0 && b >= 0)
then (a mod b) - b
else a mod b
let hardware_quot (a:integer) (b:integer) : integer =
if a < 0 && b < 0
then (abs a) / (abs b)
- else if (a < 0 && b >= 0) || (a >= 0 && b < 0)
+ else if (a < 0 && b > 0)
then (a/b) + 1
else a/b