package coq-core

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

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

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/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. | PsatzLet of 'c psatz * 'c psatz
  2. | PsatzIn of nat
  3. | PsatzSquare of 'c polC
  4. | PsatzMulC of 'c polC * 'c psatz
  5. | PsatzMulE of 'c psatz * 'c psatz
  6. | PsatzAdd of 'c psatz * 'c psatz
  7. | PsatzC of 'c
  8. | 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct