package coq-validsdp

You can search for identifiers within the package.

in-package search v0.2.0

ValidSDP

Install

Dune Dependency

sourcesup.renater.fr Edit opam file Versions (7)

Authors

Maintainers

Sources

validsdp-1.0.4.tar.gz

sha512=47f9c3b0f67cc41bec5dc97d7df4dcfec05443b2b799320b34efe0cc843f24ae11c1b6340c8c6103789338fccb5dc657729ff96e56d6d8c840d7f0dce4bf0cbd

Description

ValidSDP is a library for the Coq formal proof assistant. It provides reflexive tactics to prove multivariate inequalities involving real-valued variables and rational constants, using SDP solvers as untrusted back-ends and verified checkers based on libValidSDP.

Once installed, you can import the following modules: From Coq Require Import Reals. From ValidSDP Require Import validsdp.

Published: 07 Feb 2025

Dependencies (13)

ocamlfind build
osdp >= "1.1.1"
coq-coqeal >= "2.0.2"
coq-mathcomp-multinomials >= "2.0"
coq-libvalidsdp = version
coq-mathcomp-reals-stdlib >= "1.8.0"
coq-mathcomp-analysis >= "1.0.0" & < "1.7~"
coq-mathcomp-field >= "2.1" & < "2.4~"
coq-interval >= "4.0.0" & < "5~"
coq-flocq >= "3.3.0"
coq-bignums
coq >= "8.18" & < "8.21~"
ocaml

Dev Dependencies (1)

conf-autoconf build & dev

Used by

None

Conflicts