Path to this page:
./
lang/coq,
Theorem prover which extracts programs from proofs
Branch: CURRENT,
Version: 8.20.1,
Package name: coq-8.20.1,
Maintainer: dhollandFrom 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] [
x11/gtk3] [
graphics/adwaita-icon-theme] [
math/ocaml-num] [
lang/python37] [
x11/ocaml-lablgtk3]
Required to build:[
pkgtools/x11-links] [
x11/xcb-proto] [
x11/fixesproto4] [
pkgtools/cwrappers] [
x11/xorgproto]
Package options: coqide
Master sites:
Filesize: 7659.109 KB
Version history: (Expand)
- (2025-02-24) Updated to version: coq-8.20.1
- (2024-12-27) Updated to version: coq-8.15.2nb20
- (2024-11-17) Updated to version: coq-8.15.2nb19
- (2024-11-15) Updated to version: coq-8.15.2nb18
- (2024-11-01) Updated to version: coq-8.15.2nb17
- (2024-11-01) Updated to version: coq-8.15.2nb16
CVS history: (Expand)