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

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

Branch: pkgsrc-2012Q4, Version: 8.4nb2, Package name: coq-8.4nb2, 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/camlp5] [lang/ocaml] [x11/lablgtk] [x11/gtk2]

Required to build:
[devel/gmake] [pkgtools/x11-links] [x11/fixesproto4] [x11/inputproto] [x11/randrproto] [x11/compositeproto] [x11/renderproto] [x11/xextproto] [x11/xcb-proto] [x11/xproto]

Package options: coqide

Master sites:

SHA1: 2987aa418dd96a0df7284afe296293cb28814ef5
RMD160: 6824f9542c823c7d943a59acefb90ff9c9dbe37a
Filesize: 4037.87 KB

Version history: (Expand)