aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega/numCompat.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/numCompat.mli')
-rw-r--r--plugins/micromega/numCompat.mli11
1 files changed, 10 insertions, 1 deletions
diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index acc6be6ce0..0b4d52708f 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -25,8 +25,15 @@ module type ZArith = sig
val power_int : t -> int -> t
val quomod : t -> t -> t * t
val ppcm : t -> t -> t
+
+ (** [gcd x y] Greatest Common Divisor. Must always return a
+ positive number *)
val gcd : t -> t -> t
+
+ (** [lcm x y] Least Common Multiplier. Must always return a
+ positive number *)
val lcm : t -> t -> t
+
val to_string : t -> string
end
@@ -40,7 +47,9 @@ module type QArith = sig
val one : t
val two : t
val ten : t
- val neg_one : t
+
+ (** -1 constant *)
+ val minus_one : t
module Notations : sig
val ( // ) : t -> t -> t