Path to this page:
./
lang/coq,
Theorem prover which extracts programs from proofs
Branch: CURRENT,
Version: 8.10.2,
Package name: coq-8.10.2,
Maintainer: jaapbFrom http://coq.inria.fr/doc/tutorial.html:
Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.
Required to run:[
lang/ocaml] [
x11/gtk3] [
math/ocaml-num] [
lang/python37] [
x11/ocaml-lablgtk3]
Required to build:[
pkgtools/x11-links] [
x11/xcb-proto] [
x11/fixesproto4] [
pkgtools/cwrappers] [
x11/xorgproto]
Package options: coqide
Master sites:
SHA1: ecdb79a8b4cd76912b39e037ef52545406e63799
RMD160: a3686508b97a98b668c91a513e73f88dff02af89
Filesize: 6077.09 KB
Version history: (Expand)
- (2020-01-24) Updated to version: coq-8.10.2
- (2020-01-19) Updated to version: coq-8.9.1nb4
- (2019-09-01) Updated to version: coq-8.9.1nb3
- (2019-07-22) Updated to version: coq-8.9.1nb2
- (2019-07-21) Updated to version: coq-8.9.1nb1
- (2019-05-23) Updated to version: coq-8.9.1
CVS history: (Expand)