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 (12)

Authors

Maintainers

R

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

Sources

sha256=ea9cf8653f1e63e01f76393231d048ecd693793ca69a12f28fcc7d43a30e5e46

Description

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

Tags

category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib

Published: 20 Feb 2025

Dependencies (1)

coq-mathcomp-reals = version

Dev Dependencies

None

Used by (5)

coq-infotheo >= "0.7.5" & != "0.9.0" & < "0.9.2"
coq-libvalidsdp >= "1.0.4"
coq-mathcomp-analysis-stdlib < "1.16.0"
coq-validsdp = "1.0.4"
rocq-laproof < "2.0.1"

Conflicts

None

On This Page

Description
Dependencies (1)
Dev Dependencies
Used by (5)
Conflicts