package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.15.2.tar.gz
sha256=13a67c0a4559ae22e9765c8fdb88957b16c2b335a2d5f47e4d6d9b4b8b299926
doc/micromega_plugin/Micromega_plugin/Simplex/index.html
Module Micromega_plugin.SimplexSource
Profiling
Source
type profile_info = {number_of_successes : int;number_of_failures : int;success_pivots : int;failure_pivots : int;average_pivots : int;maximum_pivots : int;
}Simplex interface
Source
val optimise :
Vect.t ->
Polynomial.cstr list ->
(NumCompat.Q.t option * NumCompat.Q.t option) optionSource
val integer_solver :
(Polynomial.cstr * Polynomial.ProofFormat.prf_rule) list ->
Polynomial.ProofFormat.proof option