package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Mc = Micromega
val max_nb_cstr : int ref
type var = int
module Monomial : sig ... end
module MonMap : sig ... end
module Poly : sig ... end

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

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

is_strict c

  • returns

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

exception Strict
module 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

module ProofFormat : sig ... end

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

val output_cstr : out_channel -> cstr -> unit
module WithProof : sig ... end

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

module BoundWithProof : sig ... end
OCaml

Innovation. Community. Security.