package coq-core

  1. Overview
  2. No Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50

doc/micromega_plugin/Micromega_plugin/Polynomial/index.html

Module Micromega_plugin.PolynomialSource

Sourcemodule Mc = Micromega
Sourceval max_nb_cstr : int Stdlib.ref
Sourcetype var = int
Sourcemodule Monomial : sig ... end
Sourcemodule MonMap : sig ... end
Sourcemodule Poly : sig ... end

Representation of polonomial with rational coefficient. a1.m1 + ... + c where

Sourcetype cstr = {
  1. coeffs : Vect.t;
  2. op : op;
  3. cst : NumCompat.Q.t;
}
Sourceand op =
  1. | Eq
  2. | Ge
  3. | Gt
Sourceval eval_op : op -> NumCompat.Q.t -> NumCompat.Q.t -> bool
Sourceval compare_op : op -> op -> int
Sourceval opAdd : op -> op -> op
Sourceval is_strict : cstr -> bool

is_strict c

  • returns

    whether the constraint is strict i.e. c.op = Gt

Sourceexception Strict
Sourcemodule LinPoly : sig ... end

Linear(ised) polynomials represented as a Vect.t i.e a sorted association list. The constant is the coefficient of the variable 0

Sourcemodule ProofFormat : sig ... end

Proof format used by the proof-generating procedures. It is fairly close to Coq format but a bit more liberal.

Sourceval output_cstr : Stdlib.out_channel -> cstr -> unit
Sourceval opMult : op -> op -> op
Sourcemodule WithProof : sig ... end

module WithProof constructs polynomials packed with the proof that their sign is correct.

Sourcemodule BoundWithProof : sig ... end