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

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

Branch: pkgsrc-2021Q1, Version: 8.12.2nb1, Package name: coq-8.12.2nb1, Maintainer: dholland

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.



Package options: coqide

Master sites:

SHA1: 70ba8f50fb54049fe00c5ce2c29be1c829b5297d
RMD160: d691b0fc0e0b9824f15a8a26d013f8578eb095ce
Filesize: 6695.176 KB

Version history: (Expand)