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

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

Branch: pkgsrc-2018Q2, Version: 8.7.2nb3, Package name: coq-8.7.2nb3, 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/ocaml]


Package options: coqide

Master sites:

SHA1: 0175cc658aa2c93167572a33e9e39fc63f591258
RMD160: 2fd5c59e0143061e4253d68e8839ae3822d7a614
Filesize: 5619.492 KB

Version history: (Expand)