package coq
Formal proof management system
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.16.0.tar.gz
sha256=36577b55f4a4b1c64682c387de7abea932d0fd42fc0cd5406927dca344f53587
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