Paket: coq (8.20.0+dfsg-1)

[ Quellcode: coq  ]

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

• dep: libc6 (>= 2.38)

  GNU-C-Bibliothek: Laufzeitbibliotheken
  auch ein virtuelles Paket, bereitgestellt durch libc6-udeb

• dep: libcoq-core-ocaml-1ioh9 [amd64]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-core-ocaml-cg6v5 [riscv64]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-core-ocaml-sa2u3 [arm64]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-core-ocaml-zmgk8 [s390x]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-core-ocaml-zsxq8 [ppc64el]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-stdlib (= 8.20.0+dfsg-1)

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

• dep: libfindlib-ocaml-0ne56 [amd64]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-7zo87 [s390x]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-9l3r6 [riscv64]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-huq36 [ppc64el]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-s9ic8 [arm64]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libgmp10 (>= 2:6.3.0+dfsg)

  Mehrfachgenaue, arithmetische Bibliothek

• dep: libstdlib-ocaml-0d647 [arm64]

  virtuelles Paket, bereitgestellt durch libstdlib-ocaml

• dep: libstdlib-ocaml-2a614 [ppc64el]

  virtuelles Paket, bereitgestellt durch libstdlib-ocaml

• dep: libstdlib-ocaml-7l663 [amd64]

  virtuelles Paket, bereitgestellt durch libstdlib-ocaml

• dep: libstdlib-ocaml-r1af2 [s390x]

  virtuelles Paket, bereitgestellt durch libstdlib-ocaml

• dep: libstdlib-ocaml-vvst5 [riscv64]

  virtuelles Paket, bereitgestellt durch libstdlib-ocaml

• dep: libzarith-ocaml-lfk68 [s390x]

  virtuelles Paket, bereitgestellt durch libzarith-ocaml

• dep: libzarith-ocaml-mtsj7 [nicht s390x]

  virtuelles Paket, bereitgestellt durch libzarith-ocaml

• dep: ocaml

  ML language implementation with a class-based object system

• dep: ocaml-base-5.2.0

  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	Paketgröße	Größe (installiert)	Dateien
amd64	75.149,6 kB	284.268,0 kB	[Liste der Dateien]
arm64	78.955,5 kB	306.092,0 kB	[Liste der Dateien]
ppc64el	75.370,6 kB	295.469,0 kB	[Liste der Dateien]
riscv64	75.647,5 kB	295.002,0 kB	[Liste der Dateien]
s390x	75.461,0 kB	303.414,0 kB	[Liste der Dateien]