Stream: Coq users

Topic: libcoq-mathcomp-* when using Synaptic


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Huỳnh Trần Khanh (May 03 2024 at 12:22):

Try coq-stdpp. It might be in Synaptic

view this post on Zulip Huỳnh Trần Khanh (May 03 2024 at 12:23):

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

view this post on Zulip Huỳnh Trần Khanh (May 03 2024 at 12:24):

math-comp is also a good library too

view this post on Zulip 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

view this post on Zulip Heime (May 03 2024 at 13:18):

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

view this post on Zulip Julien Puydt (May 03 2024 at 17:15):

libcoq-stdpp is in Debian...


Last updated: Jun 18 2024 at 21:01 UTC