Heime (May 02 2024 at 22:31): Heime (May 02 2024 at 22:31):I have installed COQ with Synaptic Package Manager. And I see many things like
libcoq-mathcomp-*
Would one recommend to install them ?
Julien Puydt (May 03 2024 at 05:10):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.
Heime (May 03 2024 at 11:59):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.
Huỳnh Trần Khanh (May 03 2024 at 12:22):Try coq-stdpp. It might be in Synaptic
Huỳnh Trần Khanh (May 03 2024 at 12:23):It's a decent library with a bunch of common stuff
Huỳnh Trần Khanh (May 03 2024 at 12:24):math-comp is also a good library too
Huỳnh Trần Khanh (May 03 2024 at 12:24):If you can't decide what library to use probably it's worth it to read up on the libraries in the ecosystem
Heime (May 03 2024 at 13:18):I shall look into them. They are not in Synaptic.
Julien Puydt (May 03 2024 at 17:15):libcoq-stdpp is in Debian...
Last updated: Oct 13 2024 at 01:02 UTC