⚠️ Under construction ⚠️ This website will be officialy launched with the first release of Rocq 9.0 in March 2025. Until then, there may remain broken links and references to not-yet existing projects.

package coq-mathcomp-reals-stdlib

You can search for identifiers within the package.

in-package search v0.2.0

A library to link real numbers from mathematical components and Stdlib

Install

Dune Dependency

github.com Edit opam file Versions (3)

Authors

Maintainers

R

Reynald Affeldt <reynald.affeldt@aist.go.jp>

Sources

1.9.0.tar.gz

sha256=ea9cf8653f1e63e01f76393231d048ecd693793ca69a12f28fcc7d43a30e5e46

Description

This package contains a library to link real numbers for the Coq proof-assistant using the Mathematical Components library and Stdlib.

Published: 20 Feb 2025

Dependencies (1)

coq-mathcomp-reals = version

Dev Dependencies

None

Used by (4)

coq-infotheo >= "0.7.5" & != "0.9.0"
coq-libvalidsdp >= "1.0.4"
coq-mathcomp-analysis-stdlib
coq-validsdp >= "1.0.4"

Conflicts