package coq-coquelicot

  1. Overview
  2. Homepage
(patched for Coq 8.11 compatibility by MSoegtropIMC) A Coq formalization of real analysis compatible with the standard library

Install

Dune Dependency

Authors

Maintainers

Sources

1ec80657ce992fc5aa660dca86d423671f02e33c.tar.gz
sha512=c164168d3732ff9f0067e95997d6478be497244380a297ac8c092ebefa2d369246f4f8a1e6ae7d5ec6fd32e73f3b9cf96addd067b80b5bc67f3883e0933a3ce2

Description

Dependencies (5)

  1. conf-autoconf build
  2. conf-clang build
  3. conf-g++ build
  4. coq-mathcomp-ssreflect >= "1.6"
  5. coq = "8.11.0"

Dev Dependencies

None

Used by (5)

  1. coq-improper-integrals
  2. coq-interval >= "3.2.0" & < "4.11.1"
  3. coq-libvalidsdp >= "0.6.0"
  4. coq-pi-agm >= "1.2.0"
  5. coq-plouffe = "1.1.0" | >= "1.3.0" & < "1.5.0"

Conflicts

None

Rocq

Interactive Theorem Prover