package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

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

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/micromega_plugin/Micromega_plugin/Micromega/index.html

Module Micromega_plugin.MicromegaSource

Sourcetype __ = Stdlib.Obj.t
Sourcetype unit0 =
  1. | Tt
Sourceval negb : bool -> bool
Sourcetype nat =
  1. | O
  2. | S of nat
Sourcetype ('a, 'b) sum =
  1. | Inl of 'a
  2. | Inr of 'b
Sourceval fst : ('a1 * 'a2) -> 'a1
Sourceval snd : ('a1 * 'a2) -> 'a2
Sourceval app : 'a1 list -> 'a1 list -> 'a1 list
Sourcetype comparison =
  1. | Eq
  2. | Lt
  3. | Gt
Sourceval compOpp : comparison -> comparison
Sourceval add : nat -> nat -> nat
Sourceval nth : nat -> 'a1 list -> 'a1 -> 'a1
Sourceval rev_append : 'a1 list -> 'a1 list -> 'a1 list
Sourceval map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
Sourceval fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
Sourceval fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
Sourcetype positive =
  1. | XI of positive
  2. | XO of positive
  3. | XH
Sourcetype n =
  1. | N0
  2. | Npos of positive
Sourcetype z =
  1. | Z0
  2. | Zpos of positive
  3. | Zneg of positive
Sourcemodule Pos : sig ... end
Sourcemodule Coq_Pos : sig ... end
Sourcemodule N : sig ... end
Sourceval pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
Sourcemodule Z : sig ... end
Sourceval zeq_bool : z -> z -> bool
Sourcetype 'c pExpr =
  1. | PEc of 'c
  2. | PEX of positive
  3. | PEadd of 'c pExpr * 'c pExpr
  4. | PEsub of 'c pExpr * 'c pExpr
  5. | PEmul of 'c pExpr * 'c pExpr
  6. | PEopp of 'c pExpr
  7. | PEpow of 'c pExpr * n
Sourcetype 'c pol =
  1. | Pc of 'c
  2. | Pinj of positive * 'c pol
  3. | PX of 'c pol * positive * 'c pol
Sourceval p0 : 'a1 -> 'a1 pol
Sourceval p1 : 'a1 -> 'a1 pol
Sourceval peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
Sourceval mkPinj : positive -> 'a1 pol -> 'a1 pol
Sourceval mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
Sourceval mkPX : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
Sourceval mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
Sourceval mkX : 'a1 -> 'a1 -> 'a1 pol
Sourceval popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
Sourceval paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
Sourceval psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
Sourceval paddI : ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
Sourceval psubI : ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
Sourceval paddX : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
Sourceval psubX : 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
Sourceval padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
Sourceval psub : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
Sourceval pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
Sourceval pmulC : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
Sourceval pmulI : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
Sourceval pmul : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
Sourceval psquare : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
Sourceval mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
Sourceval ppow_pos : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
Sourceval ppow_N : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
Sourceval norm_aux : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
Sourcetype kind =
  1. | IsProp
  2. | IsBool
Sourcetype 'a trace =
  1. | Null
  2. | Push of 'a * 'a trace
  3. | Merge of 'a trace * 'a trace
Sourcetype ('tA, 'tX, 'aA, 'aF) gFormula =
  1. | TT of kind
  2. | FF of kind
  3. | X of kind * 'tX
  4. | A of kind * 'tA * 'aA
  5. | AND of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
  6. | OR of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
  7. | NOT of kind * ('tA, 'tX, 'aA, 'aF) gFormula
  8. | IMPL of kind * ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula
  9. | IFF of kind * ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
  10. | EQ of ('tA, 'tX, 'aA, 'aF) gFormula * ('tA, 'tX, 'aA, 'aF) gFormula
Sourceval mapX : (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
Sourceval foldA : ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
Sourceval cons_id : 'a1 option -> 'a1 list -> 'a1 list
Sourceval ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
Sourceval collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
Sourcetype rtyp = __
Sourcetype eKind = __
Sourcetype 'a bFormula = ('a, eKind, unit0, unit0) gFormula
Sourceval map_bformula : kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula
Sourcetype ('x, 'annot) clause = ('x * 'annot) list
Sourcetype ('x, 'annot) cnf = ('x, 'annot) clause list
Sourceval cnf_tt : ('a1, 'a2) cnf
Sourceval cnf_ff : ('a1, 'a2) cnf
Sourceval add_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, 'a2) clause option
Sourceval or_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause -> ('a1, 'a2) clause option
Sourceval xor_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
Sourceval or_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
Sourceval or_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
Sourceval and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
Sourcetype ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula
Sourceval is_cnf_tt : ('a1, 'a2) cnf -> bool
Sourceval is_cnf_ff : ('a1, 'a2) cnf -> bool
Sourceval and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
Sourceval or_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
Sourceval mk_and : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
Sourceval mk_or : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
Sourceval mk_impl : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
Sourceval mk_iff : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
Sourceval is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option
Sourceval xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
Sourceval radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum
Sourceval ror_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum
Sourceval xror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
Sourceval ror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
Sourceval ror_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 trace
Sourceval ror_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf * 'a2 trace
Sourceval ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 trace
Sourceval rxcnf_and : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
Sourceval rxcnf_or : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
Sourceval rxcnf_impl : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
Sourceval rxcnf_iff : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
Sourceval rxcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
Sourcetype ('term, 'annot, 'tX) to_constrT = {
  1. mkTT : kind -> 'tX;
  2. mkFF : kind -> 'tX;
  3. mkA : kind -> 'term -> 'annot -> 'tX;
  4. mkAND : kind -> 'tX -> 'tX -> 'tX;
  5. mkOR : kind -> 'tX -> 'tX -> 'tX;
  6. mkIMPL : kind -> 'tX -> 'tX -> 'tX;
  7. mkIFF : kind -> 'tX -> 'tX -> 'tX;
  8. mkNOT : kind -> 'tX -> 'tX;
  9. mkEQ : 'tX -> 'tX -> 'tX;
}
Sourceval aformula : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
Sourceval is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
Sourceval abs_and : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
Sourceval abs_or : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
Sourceval abs_not : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
Sourceval mk_arrow : 'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval abst_simpl : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval abst_and : ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval abst_or : ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval abst_impl : ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval or_is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool
Sourceval abs_iff : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval abst_iff : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval abst_eq : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval abst_form : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
Sourceval cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
Sourceval tauto_checker : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool
Sourceval cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
Sourceval cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
Sourcetype 'c polC = 'c pol
Sourcetype op1 =
  1. | Equal
  2. | NonEqual
  3. | Strict
  4. | NonStrict
Sourcetype 'c nFormula = 'c polC * op1
Sourceval opMult : op1 -> op1 -> op1 option
Sourceval opAdd : op1 -> op1 -> op1 option
Sourcetype 'c psatz =
  1. | PsatzIn of nat
  2. | PsatzSquare of 'c polC
  3. | PsatzMulC of 'c polC * 'c psatz
  4. | PsatzMulE of 'c psatz * 'c psatz
  5. | PsatzAdd of 'c psatz * 'c psatz
  6. | PsatzC of 'c
  7. | PsatzZ
Sourceval map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option
Sourceval map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option
Sourceval pexpr_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
Sourceval nformula_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
Sourceval nformula_plus_nformula : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
Sourceval eval_Psatz : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option
Sourceval check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
Sourceval check_normalised_formulas : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
Sourcetype op2 =
  1. | OpEq
  2. | OpNEq
  3. | OpLe
  4. | OpGe
  5. | OpLt
  6. | OpGt
Sourcetype 't formula = {
  1. flhs : 't pExpr;
  2. fop : op2;
  3. frhs : 't pExpr;
}
Sourceval norm : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
Sourceval psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
Sourceval padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
Sourceval popp0 : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
Sourceval normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
Sourceval xnormalise : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
Sourceval xnegate : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
Sourceval cnf_of_list : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a2 -> ('a1 nFormula, 'a2) cnf
Sourceval cnf_normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
Sourceval cnf_negate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
Sourceval xdenorm : positive -> 'a1 pol -> 'a1 pExpr
Sourceval denorm : 'a1 pol -> 'a1 pExpr
Sourceval map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr
Sourceval map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula
Sourceval simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz
Sourcetype q = {
  1. qnum : z;
  2. qden : positive;
}
Sourceval qeq_bool : q -> q -> bool
Sourceval qle_bool : q -> q -> bool
Sourceval qplus : q -> q -> q
Sourceval qmult : q -> q -> q
Sourceval qopp : q -> q
Sourceval qminus : q -> q -> q
Sourceval qinv : q -> q
Sourceval qpower_positive : q -> positive -> q
Sourceval qpower : q -> z -> q
Sourcetype 'a t =
  1. | Empty
  2. | Elt of 'a
  3. | Branch of 'a t * 'a * 'a t
Sourceval find : 'a1 -> 'a1 t -> positive -> 'a1
Sourceval singleton : 'a1 -> positive -> 'a1 -> 'a1 t
Sourceval vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
Sourceval zeval_const : z pExpr -> z option
Sourcetype zWitness = z psatz
Sourceval zWeakChecker : z nFormula list -> z psatz -> bool
Sourceval psub1 : z pol -> z pol -> z pol
Sourceval popp1 : z pol -> z pol
Sourceval padd1 : z pol -> z pol -> z pol
Sourceval normZ : z pExpr -> z pol
Sourceval zunsat : z nFormula -> bool
Sourceval zdeduce : z nFormula -> z nFormula -> z nFormula option
Sourceval xnnormalise : z formula -> z nFormula
Sourceval xnormalise0 : z nFormula -> z nFormula list
Sourceval cnf_of_list0 : 'a1 -> z nFormula list -> (z nFormula * 'a1) list list
Sourceval normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf
Sourceval xnegate0 : z nFormula -> z nFormula list
Sourceval negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
Sourceval cnfZ : kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 trace
Sourceval ceiling : z -> z -> z
Sourcetype zArithProof =
  1. | DoneProof
  2. | RatProof of zWitness * zArithProof
  3. | CutProof of zWitness * zArithProof
  4. | SplitProof of z polC * zArithProof * zArithProof
  5. | EnumProof of zWitness * zWitness * zArithProof list
  6. | ExProof of positive * zArithProof
Sourceval zgcdM : z -> z -> z
Sourceval zgcd_pol : z polC -> z * z
Sourceval zdiv_pol : z polC -> z -> z polC
Sourceval makeCuttingPlane : z polC -> z polC * z
Sourceval genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
Sourceval nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula
Sourceval is_pol_Z0 : z polC -> bool
Sourceval eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
Sourceval valid_cut_sign : op1 -> bool
Sourceval bound_var : positive -> z formula
Sourceval mk_eq_pos : positive -> positive -> positive -> z formula
Sourceval max_var : positive -> z pol -> positive
Sourceval max_var_nformulae : z nFormula list -> positive
Sourceval zChecker : z nFormula list -> zArithProof -> bool
Sourceval zTautoChecker : z formula bFormula -> zArithProof list -> bool
Sourcetype qWitness = q psatz
Sourceval qWeakChecker : q nFormula list -> q psatz -> bool
Sourceval qnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
Sourceval qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
Sourceval qunsat : q nFormula -> bool
Sourceval qdeduce : q nFormula -> q nFormula -> q nFormula option
Sourceval normQ : q pExpr -> q pol
Sourceval cnfQ : kind -> (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 trace
Sourceval qTautoChecker : q formula bFormula -> qWitness list -> bool
Sourcetype rcst =
  1. | C0
  2. | C1
  3. | CQ of q
  4. | CZ of z
  5. | CPlus of rcst * rcst
  6. | CMinus of rcst * rcst
  7. | CMult of rcst * rcst
  8. | CPow of rcst * (z, nat) sum
  9. | CInv of rcst
  10. | COpp of rcst
Sourceval z_of_exp : (z, nat) sum -> z
Sourceval q_of_Rcst : rcst -> q
Sourcetype rWitness = q psatz
Sourceval rWeakChecker : q nFormula list -> q psatz -> bool
Sourceval rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
Sourceval rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
Sourceval runsat : q nFormula -> bool
Sourceval rdeduce : q nFormula -> q nFormula -> q nFormula option
Sourceval rTautoChecker : rcst formula bFormula -> rWitness list -> bool