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

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

Branch: pkgsrc-2017Q3, Version: 8.6.1nb1, Package name: coq-8.6.1nb1, 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/ocaml]

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

Package options: coqide

Master sites:

SHA1: 5dbaf1230c297d7c11c8715c012300a51ad80f9a
RMD160: 822b0061a99de144881b1f1166eef9e92d26de7f
Filesize: 5457.823 KB

Version history: (Expand)