Module Polynomial.LinPoly
type t= Vect.t
module MonT : sig ... endval coq_poly_of_linpol : (Num.num -> 'a) -> t -> 'a Mc.pExprcoq_poly_of_linpol c p- parameter p
is a multi-variate polynomial.
- parameter c
maps a rational to a Coq polynomial coefficient.
- returns
the coq expression corresponding to polynomial
p.
val of_monomial : Monomial.t -> tof_monomial m@returns 1.x where x is the variable (index) for monomial m
val of_vect : Vect.t -> tof_vect v@returns a1.x1 + ... + an.xn This is not the identity because xi is the variable index of xi^1
val variables : t -> Micromega_plugin.Mutils.ISet.tvariables p- returns
the set of variables of the polynomial p interpreted as a multi-variate polynomial
val is_linear : t -> boolis_linear p- returns
whether the multi-variate polynomial is linear.
val is_linear_for : var -> t -> boolis_linear_for x p- returns
true if the polynomial is linear in x i.e can be written c*x+r where c is a constant and r is independent from x
val constant : Num.num -> tconstant c- returns
the constant polynomial c
val search_linear : (Num.num -> bool) -> t -> var optionval search_all_linear : (Num.num -> bool) -> t -> var listsearch_all_linear pred p- returns
all the variables x such p = a.x + b such that p is linear in x i.e x does not occur in b and a is a constant such that
pred a
val factorise : var -> t -> t * tfactorise x p- returns
a,bsuch thatp = a.x + bandxdoes not occur inb
val collect_square : t -> Monomial.t MonMap.tcollect_square p- returns
a mapping m such that m
s= s^2 for every s^2 that is a monomial ofp
val monomials : t -> Micromega_plugin.Mutils.ISet.tmonomials p- returns
the set of monomials.
val degree : t -> intdegree p- returns
return the maximum degree
val pp_var : Stdlib.out_channel -> var -> unitpp_var o vpretty-prints a monomial indexed by v.
val pp : Stdlib.out_channel -> t -> unitpp o ppretty-prints a polynomial.