./lang/coq, Theorem prover which extracts programs from proofs

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: pkgsrc-2017Q1, Version: 8.6nb2, Package name: coq-8.6nb2, Maintainer: jaapb

From 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] [lang/camlp4]


Package options: coqide

Master sites:

SHA1: 617a6f86d09dde0e409f3fa22268daf7be3f5bba
RMD160: 3d5e539c40732620e65f28988b118d2e0d663aa5
Filesize: 5409.031 KB

Version history: (Expand)