Paket: coq (8.18.0+dfsg-1 und andere)

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]

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.35)

GNU-C-Bibliothek: Laufzeitbibliotheken
auch ein virtuelles Paket, bereitgestellt durch libc6-udeb
dep: libcoq-core-ocaml-zchk9

virtuelles Paket, bereitgestellt durch libcoq-core-ocaml
dep: libcoq-stdlib (= 8.18.0+dfsg-1+b1)

Beweis-Assistent für Logik höherer Ordnung (Theorien)
dep: libfindlib-ocaml-z40n4

virtuelles Paket, bereitgestellt durch libfindlib-ocaml
dep: libgmp10 (>= 2:6.3.0+dfsg)

Mehrfachgenaue, arithmetische Bibliothek
dep: libstdlib-ocaml-058x2

virtuelles Paket, bereitgestellt durch libstdlib-ocaml
dep: libzarith-ocaml-zlfv4

virtuelles Paket, bereitgestellt durch libzarith-ocaml
dep: ocaml

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

virtuelles Paket, bereitgestellt durch ocaml-base
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: coqide

Beweis-Assistent für Logik höherer Ordnung (Gtk-Schnittstelle)

oder proofgeneral

Generisches Frontend für Beweisassistenten
sug: ledit

Zeileneditor für interaktive Programme

oder readline-editor

virtuelles Paket, bereitgestellt durch ledit, rlfe, rlwrap
sug: libcoq-core-ocaml-dev

development libraries and tools for Coq
sug: why (>= 2.19)

Paket nicht verfügbar

coq herunterladen

Download für alle verfügbaren Architekturen
Architektur	Version	Paketgröße	Größe (installiert)	Dateien
ppc64el	8.18.0+dfsg-1+b1	79.780,1 kB	319.990,0 kB	[Liste der Dateien]