Correct condition on absolute value of result.

hacspec · Jul 16, 2024 · 1c7733c · 1c7733c
1 parent f4d3d61
commit 1c7733c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/book/src/tutorial/properties.md b/book/src/tutorial/properties.md
@@ -32,7 +32,7 @@ Given `value` a field element (a `i32` whose absolute value is at most
 
 - `result ≡ value (mod FIELD_MODULUS)`;
 - the absolute value of `result` is bound as follows:
-  `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)`.
+  `|result| < FIELD_MODULUS`.
 
 It is easy to write this contract directly as `hax::requires` and
 `hax::ensures` annotations, as shown in the snippet below.