Module Pp
module Pp: sig end
val mult : Sym.t
val expt : int -> Sym.t
val is_interp : Term.t -> bool
val is_expt : Term.t -> bool
val is_mult : Term.t -> bool
val is_diophantine : Term.t -> bool
val fold : (Term.t -> int -> 'a -> 'a) -> Term.t -> 'a -> 'a
val mk_one : Term.t
val is_one : Term.t -> bool
val mk_expt : int -> Term.t -> Term.t
val mk_multl : Term.t list -> Term.t
val mk_mult : Term.t -> Term.t -> Term.t
val mk_mult_with_expt : Term.t -> int -> Term.t -> Term.t
val mk_mult_with_pp : Term.t list -> Term.t -> Term.t
val cmp1 : Term.t * int -> Term.t * int -> int
val destruct : Term.t -> Term.t * int
val insert : Term.t -> int -> Term.t list -> Term.t
val insert1 : Term.t -> Term.t list -> Term.t
val merge : Term.t list -> Term.t list -> Term.t
val mk_inv : Term.t -> Term.t
val sigma : Sym.pprod -> Term.t list -> Term.t
val map : (Term.t -> Term.t) -> Term.t -> Term.t
val to_list : Term.t -> Term.t list
Normalize a power product to a list.
val of_list : (Term.t * int) list -> Term.t
val cmp : Term.t -> Term.t -> int
val min : Term.t -> Term.t -> Term.t
val max : Term.t -> Term.t -> Term.t
Greatest common divisor of two power products. For example,
gcd 'x^2 * y' 'x * y^2 returns the triple (y, x, x * y).
x * y is the gcd of these power products.
val gcd : Term.t -> Term.t -> Term.t * Term.t * Term.t
val split : Term.t -> Term.t * Term.t
val numerator : Term.t -> Term.t
val denumerator : Term.t -> Term.t
val lcm : Term.t * Term.t -> Term.t * Term.t * Term.t
val lcm : Term.t * Term.t -> Term.t * Term.t * Term.t
val div : Term.t * Term.t -> Term.t option