Overview:

This repository contains an experimental library for real analysis for the Coq proof-assistant, specifically compatible with the Mathematical Components library. It provides mathematical structures and tools for classical analysis in Coq.

Features:

Experimental library for real analysis in Coq with Mathematical Components compatibility.
Compatible with Coq versions 8.14 to 8.17 (or dev).
Additional dependencies include various versions of MathComp ssreflect, fingroup, algebra, solvable, field, finmap, and bigenough, as well as Hierarchy Builder version 1.2.0 or later.
Contains documentation for each file and changes documented in CHANGELOG.md and CHANGELOG_UNRELEASED.md.

Summary:

This repository provides an experimental library for real analysis in Coq, specifically designed to work with the Mathematical Components library. It offers a range of mathematical structures and tools for classical analysis in Coq, with compatibility for multiple Coq versions and additional dependencies. Users can install the library using OPAM or manually build and install it. Note that the library is still in the experimental stage and may undergo changes in future versions. Documentation and changes are provided for each file in the repository.

Math Comp

Analysis