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

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

Branch: pkgsrc-2013Q2, Version: 8.4pl2nb5, Package name: coq-8.4pl2nb5, 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:
[x11/lablgtk] [x11/gtk2] [lang/camlp5]

Required to build:
[pkgtools/x11-links] [x11/randrproto] [x11/dri2proto] [x11/glproto] [x11/damageproto] [x11/renderproto] [x11/xextproto] [x11/xf86vidmodeproto] [x11/xcb-proto] [x11/fixesproto] [x11/compositeproto] [x11/xproto] [x11/inputproto] [x11/xf86driproto]

Package options: coqide

Master sites:

SHA1: adcef430b8e27663e8ea075e646112f7d4d51fa6
RMD160: 4860eaff4c8f0a235d3fcf162199eaa5fe1db2da
Filesize: 4047.961 KB

Version history: (Expand)