Stream: math-comp users

Topic: Coq Prime

view this post on Zulip Bas Spitters (Mar 07 2022 at 14:07):

Did anyone connect coq-prime to mathcomp. E.g. https://math-comp.github.io/htmldoc/mathcomp.ssreflect.prime.html
@Laurent Théry @Cyril Cohen ?

view this post on Zulip Laurent Théry (Mar 07 2022 at 14:26):

not that I know of. But do you need more than proving that prime mathcomp = prime in Z?

view this post on Zulip Bas Spitters (Mar 09 2022 at 09:30):

Thanks. That might indeed be sufficient for us. We'll see how how far it brings us.

Last updated: Jan 29 2023 at 18:03 UTC