[sledge] Document that integer division and remainder use truncation semantics

Summary:
Integer `div` and `rem` are a pair of functions that satisfy the
division rule, where the result of `div` is truncated toward zero:
```
| Div  (** Division, for integers result is truncated toward zero *)
| Rem
    (** Remainder of division, satisfies [a = b * div a b + rem a b] and
        for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
```

Reviewed By: jvillard

Differential Revision: D20584626

fbshipit-source-id: fa02a3a98

sledge/lib/exp.mli

@@ -50,8 +50,10 @@ type op2 =
   | Add  (** Addition *)
   | Sub  (** Subtraction *)
   | Mul  (** Multiplication *)
-  | Div  (** Division *)
+  | Div  (** Division, for integers result is truncated toward zero *)
-  | Rem  (** Remainder of division *)
+  | Rem
+      (** Remainder of division, satisfies [a = b * div a b + rem a b] and
+          for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
   | Udiv  (** Unsigned division *)
   | Urem  (** Remainder of unsigned division *)
   | And  (** Conjunction, boolean or bitwise *)

sledge/lib/term.mli

@@ -35,8 +35,10 @@ type op2 =
   | Le  (** Less-than-or-equal test *)
   | Ord  (** Ordered test (neither arg is nan) *)
   | Uno  (** Unordered test (some arg is nan) *)
-  | Div  (** Division *)
+  | Div  (** Division, for integers result is truncated toward zero *)
-  | Rem  (** Remainder of division *)
+  | Rem
+      (** Remainder of division, satisfies [a = b * div a b + rem a b] and
+          for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
   | And  (** Conjunction, boolean or bitwise *)
   | Or  (** Disjunction, boolean or bitwise *)
   | Xor  (** Exclusive-or, bitwise *)