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/6q2jcj71sibi5dgzz9xs7ndpk0qj1mz4-coq-ide-8.13.2.drv | ||
powerpc64le-linux | /gnu/store/h2zg0rx0dwk12mgwwv1gcilni8ic8fxb-coq-ide-8.13.2.drv | ||
mips64el-linux | /gnu/store/pa1vbm51hsb6pz6a231nbapm24mz9k0a-coq-ide-8.13.2.drv | ||
i686-linux | /gnu/store/9bhr0dhwfcwqlzwqc56rqava2qpbwpl9-coq-ide-8.13.2.drv | ||
i586-gnu | /gnu/store/q7kg0bfy3dz9cxyza1vl49nk7aczq9f9-coq-ide-8.13.2.drv | ||
armhf-linux | /gnu/store/z9864ci73wpc5mmlvybbc6ha5nmvlwa1-coq-ide-8.13.2.drv | ||
aarch64-linux | /gnu/store/kyg7l0s8y74xq352qbd968iw4m7r0mn0-coq-ide-8.13.2.drv |
Linter | Message | Location |
---|---|---|
No lint warnings ✓ |