I have installed COQ with Synaptic Package Manager. And I see many things like

libcoq-mathcomp-*

Would one recommend to install them ?

It depends on what you want to do... all of them is a possibility... and notice that some of them will pull others as deps.

Currently I want to become familiar with mathematical proving. But using actual theorems rather than toy problems. Have read that many theorems in mathematics have got a file verifying the proofs. I want to introspect those verifications in coq myself and in the process learn how proofs are verified.

Try coq-stdpp. It might be in Synaptic

It's a decent library with a bunch of common stuff

math-comp is also a good library too

If you can't decide what library to use probably it's worth it to read up on the libraries in the ecosystem

I shall look into them. They are not in Synaptic.

libcoq-stdpp is in Debian...

Last updated: Jun 18 2024 at 21:01 UTC