Package: coq (9.1.0+dfsg-1)

Links for coq

Debian Resources:

Download Source Package coq:

Maintainers:

Debian OCaml Maintainers (QA Page, Mail Archive)
Benjamin Barenblat (QA Page)
Julien Puydt (QA Page)
Ralf Treinen (QA Page)
Stéphane Glondu (QA Page)

External Resources:

Homepage [coq.inria.fr]

Similar packages:

Experimental package

Warning: This package is from the experimental distribution. That means it is likely unstable or buggy, and it may even cause data loss. Please be sure to consult the changelog and other possible documentation before using it.

proof assistant for higher-order logic (toplevel and compiler)

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

This package provides coqtop, a command line interface to Coq.

A graphical interface for Coq is provided in the coqide package. Coq can also be used with ProofGeneral, which allows proofs to be edited using emacs and xemacs. This requires the proofgeneral package to be installed.

Tags: Software Development: Compiler, Field: Mathematics, Implemented in: implemented-in::ocaml, interface::commandline, User Interface: Text-based Interactive, Role: role::program, scope::utility, Interface Toolkit: Ncurses TUI

Other Packages Related to coq

depends

recommends

suggests

enhances

dep: libc6 (>= 2.38)

Knihovna GNU C: Sdílené knihovny
also a virtual package provided by libc6-udeb
dep: libcoq-core (= 9.1.0+dfsg-1)

Asistent dokazovací logiky vyššího řádu (teorie)
dep: libcoq-core-ocaml-3d0o2 [ppc64el]

virtual package provided by libcoq-core-ocaml
dep: libcoq-core-ocaml-501i1 [s390x]

virtual package provided by libcoq-core-ocaml
dep: libcoq-core-ocaml-9jks7 [riscv64]

virtual package provided by libcoq-core-ocaml
dep: libcoq-core-ocaml-qojm9 [arm64]

virtual package provided by libcoq-core-ocaml
dep: libcoq-core-ocaml-rqof7 [amd64]

virtual package provided by libcoq-core-ocaml
dep: libfindlib-ocaml-8k3o3 [amd64]

Package not available
dep: libfindlib-ocaml-eitb4 [riscv64]

Package not available
dep: libfindlib-ocaml-itlb4 [ppc64el]

Package not available
dep: libfindlib-ocaml-svhk3 [s390x]

Package not available
dep: libfindlib-ocaml-vaiw6 [arm64]

Package not available
dep: libgmp10 (>= 2:6.3.0+dfsg)

Aritmetická knihovna s libovolnou přesností
dep: libstdlib-ocaml-2d5j3 [s390x]

Package not available
dep: libstdlib-ocaml-m4xw9 [not s390x]

Package not available
dep: libzarith-ocaml-2ofb9 [s390x]

Package not available
dep: libzarith-ocaml-h79v1 [not s390x]

Package not available
dep: ocaml

ML language implementation with a class-based object system
dep: ocaml-base-5.3.0

Package not available
dep: ocaml-findlib

management tool for OCaml libraries
dep: python3

interactive high-level object-oriented language (default python3 version)

sug: coq-doc

documentation for Coq
sug: ledit

Řádkový editor pro interaktivní programy

or readline-editor

Package not available
sug: libcoq-core-ocaml-dev

development libraries and tools for Coq
sug: rocqide

proof assistant for higher-order logic (gtk interface)

or proofgeneral

generic frontend for proof assistants
sug: why (>= 2.19)

Package not available

Download coq

Download for all available architectures
Architecture	Package Size	Installed Size	Files
amd64	38,679.5 kB	160,187.0 kB	[list of files]
arm64	42,220.8 kB	178,262.0 kB	[list of files]
ppc64el	39,383.1 kB	169,751.0 kB	[list of files]
riscv64	39,481.6 kB	168,102.0 kB	[list of files]
s390x	39,313.2 kB	175,585.0 kB	[list of files]