Paket: coq (8.3.pl4+dfsg-1 und andere)
Links für coq
Debian-Ressourcen:
- Fehlerberichte
- Entwicklerinformationen (PTS)
- Debian-Changelog
- Copyright-Datei
- Debian Patch-Nachverfolger
Quellcode-Paket coq herunterladen:
Betreuer:
- Debian OCaml Maintainers (QS-Seite, E-Mail-Archiv)
- Ralf Treinen (QS-Seite)
- Samuel Mimram (QS-Seite)
- Stéphane Glondu (QS-Seite)
Externe Ressourcen:
- Homepage [coq.inria.fr]
Ähnliche Pakete:
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.
Andere Pakete mit Bezug zu coq
|
|
|
-
- dep: coq-libs (= 8.1.pl3+dfsg-1) [m68k]
- Paket nicht verfügbar
-
- dep: coq-theories (= 8.2.pl2+dfsg-2) [hppa, powerpcspe]
- proof assistant for higher-order logic (theories)
- dep: coq-theories (= 8.3.pl2+dfsg-1) [sparc64]
- dep: coq-theories (= 8.3.pl4+dfsg-1) [nicht hppa, m68k, powerpcspe, sparc64]
-
- dep: emacsen-common
- Gemeinsame Funktionen aller Emacs-Varianten
-
- dep: libc0.1 (>= 2.7) [kfreebsd-amd64, kfreebsd-i386]
- Die »Embedded GNU C Library«: Laufzeitbibliotheken
auch ein virtuelles Paket, bereitgestellt durch libc0.1-udeb
-
- dep: libc0.3 (>= 2.7) [hurd-i386]
- Die »Embedded GNU C Library«: Laufzeitbibliotheken
auch ein virtuelles Paket, bereitgestellt durch libc0.3-udeb
-
- dep: libc6 (>= 2.11) [powerpcspe]
- Die »Embedded GNU C Library«: Laufzeitbibliotheken
auch ein virtuelles Paket, bereitgestellt durch libc6-udeb
- dep: libc6 (>= 2.2) [hppa]
- dep: libc6 (>= 2.5-5) [m68k]
- dep: libc6 (>= 2.7) [amd64, armel, i386, powerpc, sparc]
-
- dep: libcoq-ocaml-ehg05 [armel]
- virtuelles Paket, bereitgestellt durch libcoq-ocaml
-
- dep: libcoq-ocaml-m0xl3 [amd64, kfreebsd-amd64]
- virtuelles Paket, bereitgestellt durch libcoq-ocaml
-
- dep: libcoq-ocaml-nc3h8 [alpha, armhf, ia64, mips, mipsel, s390, s390x, sh4]
- virtuelles Paket, bereitgestellt durch libcoq-ocaml
-
- dep: libcoq-ocaml-rn5x5 [sparc64]
- virtuelles Paket, bereitgestellt durch libcoq-ocaml
-
- dep: libcoq-ocaml-s00f5 [hurd-i386, i386, kfreebsd-i386, powerpc, sparc]
- virtuelles Paket, bereitgestellt durch libcoq-ocaml
-
- dep: libgcc1 (>= 1:4.4.0) [armel]
- GCC Support-Bibliothek
-
- dep: libncurses5 (>= 5.6+20071006-3) [m68k]
- Gemeinsam benutzte Bibliotheken für Terminalsteuerung
-
- dep: ocaml-base-nox-3.10.2 [m68k]
- Paket nicht verfügbar
-
- dep: ocaml-base-nox-3.11.2 [hppa, powerpcspe]
- virtuelles Paket, bereitgestellt durch ocaml-base-nox
-
- dep: ocaml-base-nox-3.12.0 [sparc64]
- virtuelles Paket, bereitgestellt durch ocaml-base-nox
-
- dep: ocaml-base-nox-3.12.1 [nicht hppa, m68k, powerpcspe, sparc64]
- virtuelles Paket, bereitgestellt durch ocaml-base-nox
-
- dep: tex-common (>= 1.10) [m68k]
- Gemeinsame Infrastruktur zum Erstellen und Installieren von TeX
-
- rec: coqide [nicht hppa, m68k, powerpcspe, sparc64]
- Beweis-Assistent für Logik höherer Ordnung (Gtk-Schnittstelle)
- oder proofgeneral
- generic frontend for proof assistants
-
- rec: coqide [hppa, m68k, powerpcspe, sparc64]
- Beweis-Assistent für Logik höherer Ordnung (Gtk-Schnittstelle)
- oder proofgeneral-coq
- generic interface for proof assistants - coq support
-
- sug: cle [m68k]
- Paket nicht verfügbar
-
- sug: coq-doc
- documentation for Coq
-
- sug: ledit [m68k]
- Zeileneditor für interaktive Programme
-
- sug: ledit [nicht m68k]
- Zeileneditor für interaktive Programme
- oder readline-editor
- virtuelles Paket, bereitgestellt durch ledit, rlfe, rlwrap
-
- sug: libcoq-ocaml-dev [nicht m68k]
- development libraries and tools for Coq
-
- sug: ocaml-nox [nicht m68k]
- ML-Implementierung mit einem klassenbasierten Objektsystem (ohne X)
- sug: ocaml-nox (>= 3.08) [m68k]
-
- sug: proofgeneral [nicht hppa, m68k, powerpcspe, sparc64]
- generic frontend for proof assistants
-
- sug: proofgeneral-coq [hppa, m68k, powerpcspe, sparc64]
- generic interface for proof assistants - coq support
-
- sug: why (>= 2.19) [nicht m68k]
- Software verification tool
coq herunterladen
| Architektur | Version | Paketgröße | Größe (installiert) | Dateien |
|---|---|---|---|---|
| alpha (inoffizielle Portierung) | 8.3.pl4+dfsg-1 | 1.769,9 kB | 8.225,0 kB | [Liste der Dateien] |
| amd64 | 8.3.pl4+dfsg-1 | 5.542,9 kB | 18.432,0 kB | [Liste der Dateien] |
| armel | 8.3.pl4+dfsg-1 | 5.967,2 kB | 17.898,0 kB | [Liste der Dateien] |
| armhf | 8.3.pl4+dfsg-1 | 1.770,7 kB | 8.225,0 kB | [Liste der Dateien] |
| hppa | 8.2.pl2+dfsg-2 | 3.608,8 kB | 18.268,0 kB | [Liste der Dateien] |
| hurd-i386 | 8.3.pl4+dfsg-1+b1 | 4.941,7 kB | 15.044,0 kB | [Liste der Dateien] |
| i386 | 8.3.pl4+dfsg-1 | 4.946,3 kB | 15.045,0 kB | [Liste der Dateien] |
| ia64 | 8.3.pl4+dfsg-1+b1 | 1.770,0 kB | 8.225,0 kB | [Liste der Dateien] |
| kfreebsd-amd64 | 8.3.pl4+dfsg-1 | 5.537,4 kB | 18.311,0 kB | [Liste der Dateien] |
| kfreebsd-i386 | 8.3.pl4+dfsg-1 | 4.940,5 kB | 14.925,0 kB | [Liste der Dateien] |
| m68k (inoffizielle Portierung) | 8.1.pl3+dfsg-1+b2 | 4.014,9 kB | 18.580,0 kB | [Liste der Dateien] |
| mips | 8.3.pl4+dfsg-1 | 1.768,9 kB | 8.225,0 kB | [Liste der Dateien] |
| mipsel | 8.3.pl4+dfsg-1+b1 | 1.768,6 kB | 8.225,0 kB | [Liste der Dateien] |
| powerpc | 8.3.pl4+dfsg-1 | 5.427,1 kB | 15.876,0 kB | [Liste der Dateien] |
| powerpcspe (inoffizielle Portierung) | 8.2.pl2+dfsg-2 | 3.606,8 kB | 18.260,0 kB | [Liste der Dateien] |
| s390 | 8.3.pl4+dfsg-1 | 1.770,0 kB | 8.225,0 kB | [Liste der Dateien] |
| s390x | 8.3.pl4+dfsg-1 | 1.771,4 kB | 8.225,0 kB | [Liste der Dateien] |
| sh4 (inoffizielle Portierung) | 8.3.pl4+dfsg-1 | 1.770,3 kB | 8.225,0 kB | [Liste der Dateien] |
| sparc | 8.3.pl4+dfsg-1 | 5.289,9 kB | 15.807,0 kB | [Liste der Dateien] |
| sparc64 (inoffizielle Portierung) | 8.3.pl2+dfsg-1 | 1.763,2 kB | 8.432,0 kB | [Liste der Dateien] |
