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/dbwzfam939w8xwa7ms5dfjg04c09q7k3-coq-8.15.1.drv | ||
riscv64-linux | /gnu/store/bd8sv2xn0jn5lxqi97vkbyzzmvll266m-coq-8.15.1.drv | ||
powerpc-linux | /gnu/store/gmvn1cc7g1zbsazhwj8ajnarq7dsk8xr-coq-8.15.1.drv | ||
powerpc64le-linux | /gnu/store/4d131gmgw9ssbvi45zmlzb7lk0any0g7-coq-8.15.1.drv | ||
mips64el-linux | /gnu/store/p532ybc6xm7z2f3l2y8nk4icw89rwsb6-coq-8.15.1.drv | ||
i686-linux | /gnu/store/xqmk5j406fp2aakn7djhllbiwz9q3grm-coq-8.15.1.drv | ||
i586-gnu | /gnu/store/q4yp1nvhl3cl1zkcrh3h4s3pcii1zykw-coq-8.15.1.drv | ||
armhf-linux | /gnu/store/2pbpqna4a6z20v43d3vibgqqz1284khm-coq-8.15.1.drv | ||
aarch64-linux | /gnu/store/6wr3x1drmrsx2207jw7z70qzlldcrbi8-coq-8.15.1.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |