Proof assistant for higher-order logic
Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/6lg8513s3dsvk9ndhnz3i1y067rzzr93-coq-8.15.0.drv | ||
| riscv64-linux | /gnu/store/vcf0nmvifscxl833krgdayci1s6an0bs-coq-8.15.0.drv | ||
| powerpc-linux | /gnu/store/rzypgz5qm24rczmm6xd5518y38i30r51-coq-8.15.0.drv | ||
| powerpc64le-linux | /gnu/store/qb13ghf08asn1gm8ylgi3r7gf8fkd9bv-coq-8.15.0.drv | ||
| mips64el-linux | /gnu/store/sv5g1w94rs1ag171mahp9nvbajv05ihd-coq-8.15.0.drv | ||
| i686-linux | /gnu/store/m0g5q4mgyh9nqmbbm16k78kwl23hmvbg-coq-8.15.0.drv | ||
| i586-gnu | /gnu/store/p8kd9bhcpyncx5gjlry04lbfyfrz436x-coq-8.15.0.drv | ||
| armhf-linux | /gnu/store/kavk03qwxh3i7ga0vdksk46gab76sb5x-coq-8.15.0.drv | ||
| aarch64-linux | /gnu/store/nf7vb017pcwkqbw61569ad11w8z20zy6-coq-8.15.0.drv |
| Linter | Message | Location |
|---|---|---|
| No lint warnings ✓ | ||