Up – Package index » rocq-runtime » Library micromega_plugin » Micromega_plugin » Polynomial » BoundWithProof

Module `Polynomial.BoundWithProof`Source

Sourcetype t

Sourceval make : WithProof.t -> t option

Sourceval mul_bound : t -> t -> t option

Sourceval bound : t -> Vect.Bound.t

Sourceval proof : t -> WithProof.t