Mathematical Components for Coq
Mathematical Components for Coq has its origins in the formal proof of the Four Colour Theorem. Since then it has grown to cover many areas of mathematics and has been used for large scale projects like the formal proof of the Odd Order Theorem.
The library is written using the Ssreflect proof language that is an integral part of the distribution.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/wcjxdvfvl5qf4pv98jzpni90581p59h0-coq-mathcomp-1.10.0.drv | ||
| mips64el-linux | /gnu/store/xwq6pqdvsmgzr084jmd4j39j5pyk9fsm-coq-mathcomp-1.10.0.drv | ||
| i686-linux | /gnu/store/sq5fsybnfssw1hpq12ncd4s7b3qmml3b-coq-mathcomp-1.10.0.drv | ||
| armhf-linux | /gnu/store/f47jw3w7lsnl6d7djj6wkpyrcbfcb0yq-coq-mathcomp-1.10.0.drv | ||
| aarch64-linux | /gnu/store/a9jrbyq9r4g5k6nnwlyn5hncrpw9mlw5-coq-mathcomp-1.10.0.drv |
| Linter | Message | Location |
|---|---|---|
| No lint warnings ✓ | ||