Paket: coq (9.1.0+dfsg-1)

Links für coq

Debian-Ressourcen:

Quellcode-Paket coq herunterladen:

Betreuer:

Debian OCaml Maintainers (QS-Seite, E-Mail-Archiv)
Benjamin Barenblat (QS-Seite)
Julien Puydt (QS-Seite)
Ralf Treinen (QS-Seite)
Stéphane Glondu (QS-Seite)

Externe Ressourcen:

Homepage [coq.inria.fr]

Experimentelles Paket

Warnung: Dieses Paket stammt aus der Experimental-Distribution. Dies bedeutet, dass es höchstwahrscheinlich instabil oder fehlerhaft ist und sogar Datenverlust verursachen kann. Bitte lesen Sie den Changelog und andere möglicherweise verfügbare Dokumentation, bevor Sie es benutzen.

Beweis-Assistent für Logik höherer Ordnung (Toplevel und Compiler)

Coq ist ein Beweis-Assistent für Logik höherer Ordnung. Er ermöglicht die Entwicklung von Computerprogrammen, die konsistent mit ihrer formalen Spezifikation sind. Er wird mittels Objective Caml und Camlp5 entwickelt.

Dieses Paket enthält coqtop, eine Befehlszeilen-Schnittstelle zu Coq.

Eine grafische Oberfläche für Coq finden Sie im Paket coqide. Coq kann auch mit ProofGeneral verwendet werden, was die Bearbeitung der Beweise mit Emacs und XEmacs ermöglicht. Dies erfordert die Installation des Pakets proofgeneral.

Markierungen: Software-Entwicklung: Compiler, Feld: Mathematik, Implementiert in: implemented-in::ocaml, interface::commandline, Benutzer-Schnittstellen: Text-basiert interaktiv, Rolle: role::program, scope::utility, GUI-Baukasten: Ncurses TUI

Andere Pakete mit Bezug zu coq

hängt ab von

empfiehlt

schlägt vor

erweitert

dep: libc6 (>= 2.38)

GNU-C-Bibliothek: Laufzeitbibliotheken
auch ein virtuelles Paket, bereitgestellt durch libc6-udeb
dep: libcoq-core (= 9.1.0+dfsg-1)

Beweis-Assistent für Logik höherer Ordnung (Theorien)
dep: libcoq-core-ocaml-3d0o2 [ppc64el]

virtuelles Paket, bereitgestellt durch libcoq-core-ocaml
dep: libcoq-core-ocaml-501i1 [s390x]

virtuelles Paket, bereitgestellt durch libcoq-core-ocaml
dep: libcoq-core-ocaml-9jks7 [riscv64]

virtuelles Paket, bereitgestellt durch libcoq-core-ocaml
dep: libcoq-core-ocaml-qojm9 [arm64]

virtuelles Paket, bereitgestellt durch libcoq-core-ocaml
dep: libcoq-core-ocaml-rqof7 [amd64]

virtuelles Paket, bereitgestellt durch libcoq-core-ocaml
dep: libfindlib-ocaml-8k3o3 [amd64]

Paket nicht verfügbar
dep: libfindlib-ocaml-eitb4 [riscv64]

Paket nicht verfügbar
dep: libfindlib-ocaml-itlb4 [ppc64el]

Paket nicht verfügbar
dep: libfindlib-ocaml-svhk3 [s390x]

Paket nicht verfügbar
dep: libfindlib-ocaml-vaiw6 [arm64]

Paket nicht verfügbar
dep: libgmp10 (>= 2:6.3.0+dfsg)

Mehrfachgenaue, arithmetische Bibliothek
dep: libstdlib-ocaml-2d5j3 [s390x]

Paket nicht verfügbar
dep: libstdlib-ocaml-m4xw9 [nicht s390x]

Paket nicht verfügbar
dep: libzarith-ocaml-2ofb9 [s390x]

Paket nicht verfügbar
dep: libzarith-ocaml-h79v1 [nicht s390x]

Paket nicht verfügbar
dep: ocaml

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

Paket nicht verfügbar
dep: ocaml-findlib

Verwaltungswerkzeug für OCaml-Bibliotheken
dep: python3

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

sug: coq-doc

documentation for Coq
sug: ledit

Zeileneditor für interaktive Programme

oder readline-editor

Paket nicht verfügbar
sug: libcoq-core-ocaml-dev

development libraries and tools for Coq
sug: rocqide

proof assistant for higher-order logic (gtk interface)

oder proofgeneral

Generisches Frontend für Beweisassistenten
sug: why (>= 2.19)

Paket nicht verfügbar

coq herunterladen

Download für alle verfügbaren Architekturen
Architektur	Paketgröße	Größe (installiert)	Dateien
amd64	38.679,5 kB	160.187,0 kB	[Liste der Dateien]
arm64	42.220,8 kB	178.262,0 kB	[Liste der Dateien]
ppc64el	39.383,1 kB	169.751,0 kB	[Liste der Dateien]
riscv64	39.481,6 kB	168.102,0 kB	[Liste der Dateien]
s390x	39.313,2 kB	175.585,0 kB	[Liste der Dateien]