package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type vname = string
type term =
  1. | Zero
  2. | Const of NumCompat.Q.t
  3. | Var of vname
  4. | Opp of term
  5. | Add of term * term
  6. | Sub of term * term
  7. | Mul of term * term
  8. | Pow of term * int
val output_term : out_channel -> term -> unit
type positivstellensatz =
  1. | Axiom_eq of int
  2. | Axiom_le of int
  3. | Axiom_lt of int
  4. | Rational_eq of NumCompat.Q.t
  5. | Rational_le of NumCompat.Q.t
  6. | Rational_lt of NumCompat.Q.t
  7. | Square of term
  8. | Monoid of int list
  9. | Eqmul of term * positivstellensatz
  10. | Sum of positivstellensatz * positivstellensatz
  11. | Product of positivstellensatz * positivstellensatz
val output_psatz : out_channel -> positivstellensatz -> unit