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

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

Branch: pkgsrc-2016Q1, Version: 8.5nb1, Package name: coq-8.5nb1, 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] [lang/camlp5]

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

Package options: coqide

Master sites:

SHA1: 0a0d124b1869d7e20cfcf3f71f086488c146f883
RMD160: 551d35ac96436d98112fa1a17bcc075ee307c627
Filesize: 5221.341 KB

Version history: (Expand)