⚠️ 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

You can search for identifiers within the package.

in-package search v0.2.0

A library for real numbers for mathematical components

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 for real numbers for the Coq proof-assistant and using the Mathematical Components library.

Published: 20 Feb 2025

Dependencies (1)

coq-mathcomp-classical = version

Dev Dependencies

None

Used by (3)

coq-mathcomp-analysis >= "1.9.0"
coq-mathcomp-experimental-reals >= "1.9.0"
coq-mathcomp-reals-stdlib >= "1.9.0"

Conflicts