The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Hi, 

I don't know about Coquelicot, but note that there is also math-
comp/analysis (https://github.com/math-comp/analysis/), which may well
have most of the things you mention and is designed to be used together
with mathcomp. 

Best,
Christian

On Wed, 2021-05-05 at 20:26 +0530, Mohit Tekriwal wrote:
> Hello,
> 
> I wanted to know if there is any work on interaction between Coquelicot
> and mathcomp libraries. I know that mathcomp has a rich  formalization
> of linear algebra. Coquelicot on the other hand has a rich
> formalization of reals and other analysis of real valued functions like
> limits, derivatives, integrals etc. If I were to define a real valued
> matrix in mathcomp and be able to leverage the Coquelicot formalization
> of reals for analysis, how would I go about doing that ? Are there any
> existing work, I can refer to ?
> 
> Thanking you,
> Mohit Tekriwal,
> PhD candidate, 
> University of Michigan.