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

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

Branch: pkgsrc-2018Q1, Version: 8.7.1nb2, Package name: coq-8.7.1nb2, 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/camlp5]


Package options: coqide

Master sites:

SHA1: ea4c4bbed3dc1a5550bbb7e2923ed751f9ad2be6
RMD160: 405d24ba9f0eda5b72e8bd0ed0778390cc444bf0
Filesize: 5538.213 KB

Version history: (Expand)