package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type __ = Obj.t
type unit0 =
  1. | Tt
val negb : bool -> bool
type nat =
  1. | O
  2. | S of nat
type ('a, 'b) sum =
  1. | Inl of 'a
  2. | Inr of 'b
val fst : ('a1 * 'a2) -> 'a1
val snd : ('a1 * 'a2) -> 'a2
val app : 'a1 list -> 'a1 list -> 'a1 list
type comparison =
  1. | Eq
  2. | Lt
  3. | Gt
val compOpp : comparison -> comparison
val add : nat -> nat -> nat
val nth : nat -> 'a1 list -> 'a1 -> 'a1
val rev_append : 'a1 list -> 'a1 list -> 'a1 list
val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
type positive =
  1. | XI of positive
  2. | XO of positive
  3. | XH
type n =
  1. | N0
  2. | Npos of positive
type z =
  1. | Z0
  2. | Zpos of positive
  3. | Zneg of positive
module Pos : sig ... end
module Coq_Pos : sig ... end
module N : sig ... end
val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
module Z : sig ... end
val zeq_bool : z -> z -> bool
type '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
type 'c pol =
  1. | Pc of 'c
  2. | Pinj of positive * 'c pol
  3. | PX of 'c pol * positive * 'c pol
val p0 : 'a1 -> 'a1 pol
val p1 : 'a1 -> 'a1 pol
val peq : ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> bool
val mkPinj : positive -> 'a1 pol -> 'a1 pol
val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol
val mkPX : 'a1 -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol
val mkX : 'a1 -> 'a1 -> 'a1 pol
val popp : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol
val paddI : ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val psubI : ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val paddX : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val psubX : 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val psub : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
val pmulC : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
val pmulI : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
val pmul : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val psquare : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
val ppow_pos : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
val ppow_N : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
val norm_aux : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
type kind =
  1. | IsProp
  2. | IsBool
type 'a trace =
  1. | Null
  2. | Push of 'a * 'a trace
  3. | Merge of 'a trace * 'a trace
type ('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
val mapX : (kind -> 'a2 -> 'a2) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula
val foldA : ('a5 -> 'a3 -> 'a5) -> kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5
val cons_id : 'a1 option -> 'a1 list -> 'a1 list
val ids_of_formula : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a4 list
val collect_annot : kind -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a3 list
type rtyp = __
type eKind = __
type 'a bFormula = ('a, eKind, unit0, unit0) gFormula
val map_bformula : kind -> ('a1 -> 'a2) -> ('a1, 'a3, 'a4, 'a5) gFormula -> ('a2, 'a3, 'a4, 'a5) gFormula
type ('x, 'annot) clause = ('x * 'annot) list
type ('x, 'annot) cnf = ('x, 'annot) clause list
val cnf_tt : ('a1, 'a2) cnf
val cnf_ff : ('a1, 'a2) cnf
val add_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, 'a2) clause option
val or_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause -> ('a1, 'a2) clause option
val xor_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val or_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val or_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula
val is_cnf_tt : ('a1, 'a2) cnf -> bool
val is_cnf_ff : ('a1, 'a2) cnf -> bool
val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val or_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
val 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
val 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
val 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
val 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
val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option
val 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
val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum
val ror_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum
val xror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
val ror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
val ror_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 trace
val ror_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf * 'a2 trace
val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 trace
val 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
val 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
val 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
val 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
val 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
type ('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;
}
val aformula : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
val 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
val 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
val 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
val mk_arrow : 'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
val abst_simpl : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
val 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
val 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
val 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
val or_is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool
val 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
val 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
val 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
val abst_form : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
val 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
val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
val cltb : ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
type 'c polC = 'c pol
type op1 =
  1. | Equal
  2. | NonEqual
  3. | Strict
  4. | NonStrict
type 'c nFormula = 'c polC * op1
val opMult : op1 -> op1 -> op1 option
val opAdd : op1 -> op1 -> op1 option
type '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
val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option
val map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option
val pexpr_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option
val nformula_times_nformula : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
val nformula_plus_nformula : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
val eval_Psatz : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option
val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
val check_normalised_formulas : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
type op2 =
  1. | OpEq
  2. | OpNEq
  3. | OpLe
  4. | OpGe
  5. | OpLt
  6. | OpGt
type 't formula = {
  1. flhs : 't pExpr;
  2. fop : op2;
  3. frhs : 't pExpr;
}
val norm : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
val popp0 : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
val normalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
val xnormalise : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
val xnegate : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
val cnf_of_list : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a2 -> ('a1 nFormula, 'a2) cnf
val 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
val 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
val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
val denorm : 'a1 pol -> 'a1 pExpr
val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr
val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula
val simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz
type q = {
  1. qnum : z;
  2. qden : positive;
}
val qeq_bool : q -> q -> bool
val qle_bool : q -> q -> bool
val qplus : q -> q -> q
val qmult : q -> q -> q
val qopp : q -> q
val qminus : q -> q -> q
val qinv : q -> q
val qpower_positive : q -> positive -> q
val qpower : q -> z -> q
type 'a t =
  1. | Empty
  2. | Elt of 'a
  3. | Branch of 'a t * 'a * 'a t
val find : 'a1 -> 'a1 t -> positive -> 'a1
val singleton : 'a1 -> positive -> 'a1 -> 'a1 t
val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
val zeval_const : z pExpr -> z option
type zWitness = z psatz
val zWeakChecker : z nFormula list -> z psatz -> bool
val psub1 : z pol -> z pol -> z pol
val popp1 : z pol -> z pol
val padd1 : z pol -> z pol -> z pol
val normZ : z pExpr -> z pol
val zunsat : z nFormula -> bool
val zdeduce : z nFormula -> z nFormula -> z nFormula option
val xnnormalise : z formula -> z nFormula
val xnormalise0 : z nFormula -> z nFormula list
val cnf_of_list0 : 'a1 -> z nFormula list -> (z nFormula * 'a1) list list
val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf
val xnegate0 : z nFormula -> z nFormula list
val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
val cnfZ : kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 trace
val ceiling : z -> z -> z
type 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
val zgcdM : z -> z -> z
val zgcd_pol : z polC -> z * z
val zdiv_pol : z polC -> z -> z polC
val makeCuttingPlane : z polC -> z polC * z
val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option
val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula
val is_pol_Z0 : z polC -> bool
val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option
val valid_cut_sign : op1 -> bool
val bound_var : positive -> z formula
val mk_eq_pos : positive -> positive -> positive -> z formula
val max_var : positive -> z pol -> positive
val max_var_nformulae : z nFormula list -> positive
val zChecker : z nFormula list -> zArithProof -> bool
val zTautoChecker : z formula bFormula -> zArithProof list -> bool
type qWitness = q psatz
val qWeakChecker : q nFormula list -> q psatz -> bool
val qnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val qunsat : q nFormula -> bool
val qdeduce : q nFormula -> q nFormula -> q nFormula option
val normQ : q pExpr -> q pol
val cnfQ : kind -> (q formula, 'a1, 'a2, 'a3) tFormula -> (q nFormula, 'a1) cnf * 'a1 trace
val qTautoChecker : q formula bFormula -> qWitness list -> bool
type 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
val z_of_exp : (z, nat) sum -> z
val q_of_Rcst : rcst -> q
type rWitness = q psatz
val rWeakChecker : q nFormula list -> q psatz -> bool
val rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf
val runsat : q nFormula -> bool
val rdeduce : q nFormula -> q nFormula -> q nFormula option
val 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