diff options
Diffstat (limited to 'lib/Camlcoq.ml')
-rw-r--r-- | lib/Camlcoq.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 5b5d37ee..63a31181 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -170,6 +170,8 @@ module Z = struct let add = Z.add let sub = Z.sub let mul = Z.mul + let div = Z.div + let modulo = Z.modulo let eq x y = (Z.compare x y = Eq) let lt x y = (Z.compare x y = Lt) let gt x y = (Z.compare x y = Gt) @@ -247,9 +249,13 @@ module Z = struct let to_string = dec + let is_power2 x = + gt x zero && eq (Z.coq_land x (pred x)) zero + let (+) = add let (-) = sub let ( * ) = mul + let ( / ) = div let (=) = eq let (<) = lt let (<=) = le |