module Monomials: sig end
Iterators over monomials.
type pred = Mpa.Q.t -> Term.t -> bool
val is_true : pred
val is_pos : pred
val is_neg : pred
val is_var : Term.t -> pred
val mapq : (Mpa.Q.t -> Mpa.Q.t) -> Term.t -> Term.t
val fold : pred -> (Mpa.Q.t -> Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
Folding over the non-constant monomials of an arithmetic term.
val exists : pred -> Term.t -> bool
val for_all : pred -> Term.t -> bool
val variable_choose : pred -> Term.t -> Term.t
val coefficient_choose : pred -> Term.t -> Mpa.Q.t
module Pos: sig end
Iterators over positive monomials.
module Neg: sig end
Iterators over negative monomials.