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

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

Branch: pkgsrc-2019Q1, Version: 8.9.0, Package name: coq-8.9.0, 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/python27] [lang/camlp5]


Package options: coqide

Master sites:

SHA1: 8833deafd57649f875f15c0739c8ac1ffe06aeda
RMD160: b587d945a5eb0366c7a7b280f1ff08940c800a60
Filesize: 5851.768 KB

Version history: (Expand)