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

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

Branch: pkgsrc-2016Q3, Version: 8.5pl1nb1, Package name: coq-8.5pl1nb1, 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/gtk2] [x11/ocaml-lablgtk]

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

Package options: coqide

Master sites:

SHA1: 92722ffc2be6948e0074b211bb556ad4b911ebd6
RMD160: 04c540ab1033fd6b0e4c121b73ed56557708e7a5
Filesize: 5240.99 KB

Version history: (Expand)