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

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

Branch: pkgsrc-2019Q2, Version: 8.9.1, Package name: coq-8.9.1, 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:
[math/ocaml-num] [lang/camlp5]


Package options: coqide

Master sites:

SHA1: d26646b33922bcd9eb44ef80162f8d0513784e46
RMD160: d82a0f7d31c0e5d7b8b566cd15d7ff9f724c250b
Filesize: 5861.299 KB

Version history: (Expand)