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/f9aj2hf8n28hvqng2fb70srjpirhfzs0-coq-8.15.2.drv | ||
riscv64-linux | /gnu/store/lhrap7pypm1r0a313zm2vsyqgi8a3y36-coq-8.15.2.drv | ||
powerpc-linux | /gnu/store/h8zkyq3jxhwhbk4s36f620vqlac99qzl-coq-8.15.2.drv | ||
powerpc64le-linux | /gnu/store/4bkpgiivgiqkzgf3mb334bjccm5wmbxb-coq-8.15.2.drv | ||
mips64el-linux | /gnu/store/djfx68w5a6sh9033pw6dckp4xlsn6642-coq-8.15.2.drv | ||
i686-linux | /gnu/store/nym7nsix4abwcm2s9agdc2zv0pf7fmmb-coq-8.15.2.drv | ||
i586-gnu | /gnu/store/wdl17gzdf20ngyvcr50i7zxr6pwz0dq3-coq-8.15.2.drv | ||
armhf-linux | /gnu/store/dnziz4ji0hp2h3czd6ak5cb5nvq3d3m8-coq-8.15.2.drv | ||
aarch64-linux | /gnu/store/zassn3hl1b3vpsq5zrryvrmcs3k3ypal-coq-8.15.2.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |