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

[ 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: coq-libs (= 8.1.pl3+dfsg-1) [m68k]

  Paket nicht verfügbar

• dep: coq-theories (= 8.12.0-3+b3) [alpha, hppa, ia64, sh4, sparc64, x32]

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

• dep: emacsen-common [m68k]

  Gemeinsame Funktionen aller Emacs-Varianten

• dep: libc6 (>= 2.38) [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

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

  dep: libc6 (>= 2.5-5) [m68k]

• dep: libcoq-core-ocaml-5ojv3 [ppc64el]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

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

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

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

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

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

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-core-ocaml-y4zh2 [amd64]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-core-ocaml-yi844 [ppc64]

  virtuelles Paket, bereitgestellt durch libcoq-core-ocaml

• dep: libcoq-ocaml-4s3g2 [alpha, hppa, ia64, sh4, sparc64, x32]

  virtuelles Paket, bereitgestellt durch libcoq-ocaml

• dep: libcoq-stdlib (= 8.19.1+dfsg-3) [ppc64]

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

  dep: libcoq-stdlib (= 8.20.0+dfsg-1+b1) [amd64, arm64, ppc64el, riscv64, s390x]

• dep: libfindlib-ocaml-5g6y9 [riscv64]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-81xe8 [s390x]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-adir6 [arm64]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-l8hb7 [ppc64]

  Paket nicht verfügbar

• dep: libfindlib-ocaml-obzq1 [amd64]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libfindlib-ocaml-v7wi5 [ppc64el]

  virtuelles Paket, bereitgestellt durch libfindlib-ocaml

• dep: libgmp10 (>= 2:6.3.0+dfsg) [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  Mehrfachgenaue, arithmetische Bibliothek

• dep: libncurses5 (>= 5.6+20071006-3) [m68k]

  Paket nicht verfügbar

• dep: libnum-ocaml-3st20 [alpha, hppa, ia64, sh4, sparc64, x32]

  virtuelles Paket, bereitgestellt durch libnum-ocaml

• dep: libstdlib-ocaml-fxjy5 [amd64, arm64, ppc64el, riscv64]

  virtuelles Paket, bereitgestellt durch libstdlib-ocaml

• dep: libstdlib-ocaml-gats1 [ppc64]

  Paket nicht verfügbar

• dep: libstdlib-ocaml-ke4j9 [s390x]

  virtuelles Paket, bereitgestellt durch libstdlib-ocaml

• dep: libzarith-ocaml-avzf2 [ppc64]

  Paket nicht verfügbar

• dep: libzarith-ocaml-f1se9 [amd64, arm64, ppc64el, riscv64]

  virtuelles Paket, bereitgestellt durch libzarith-ocaml

• dep: libzarith-ocaml-i2hh0 [s390x]

  virtuelles Paket, bereitgestellt durch libzarith-ocaml

• dep: ocaml [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  ML language implementation with a class-based object system

• dep: ocaml-base-4.14.1 [ppc64]

  virtuelles Paket, bereitgestellt durch ocaml-base

• dep: ocaml-base-5.3.0 [amd64, arm64, ppc64el, riscv64, s390x]

  virtuelles Paket, bereitgestellt durch ocaml-base

• dep: ocaml-base-nox-3.10.2 [m68k]

  Paket nicht verfügbar

• dep: ocaml-base-nox-4.11.1 [alpha, hppa, ia64, sh4, sparc64, x32]

  Paket nicht verfügbar

• dep: ocaml-findlib [nicht m68k]

  Verwaltungswerkzeug für OCaml-Bibliotheken

• dep: ocaml-nox [alpha, hppa, ia64, sh4, sparc64, x32]

  transitional package for ocaml

• dep: python3 [nicht m68k]

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

• dep: tex-common (>= 1.10) [m68k]

  Gemeinsame Infrastruktur zum Erstellen und Installieren von TeX

• rec: coqide

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

  oder proofgeneral-coq

  Paket nicht verfügbar

• sug: cle [m68k]

  Paket nicht verfügbar

• sug: coq-doc

  documentation for Coq

• sug: coqide [nicht m68k]

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

  oder proofgeneral

  Generisches Frontend für Beweisassistenten

• 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-core-ocaml-dev [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  development libraries and tools for Coq

• sug: libcoq-ocaml-dev [alpha, hppa, ia64, sh4, sparc64, x32]

  development libraries and tools for Coq

• sug: ocaml-nox (>= 3.08) [m68k]

  transitional package for ocaml

• sug: proofgeneral-coq [m68k]

  Paket nicht verfügbar

• sug: why (>= 2.19) [nicht m68k]

  Paket nicht verfügbar

coq herunterladen

Download für alle verfügbaren Architekturen

Architektur	Version	Paketgröße	Größe (installiert)	Dateien
alpha (inoffizielle Portierung)	8.12.0-3+b3	103.380,6 kB	412.882,0 kB	[Liste der Dateien]
amd64	8.20.0+dfsg-1+b1	68.424,8 kB	255.449,0 kB	[Liste der Dateien]
arm64	8.20.0+dfsg-1+b1	72.572,3 kB	276.904,0 kB	[Liste der Dateien]
hppa (inoffizielle Portierung)	8.12.0-3+b3	103.393,2 kB	412.952,0 kB	[Liste der Dateien]
ia64 (inoffizielle Portierung)	8.12.0-3+b3	103.379,1 kB	412.878,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]
ppc64 (inoffizielle Portierung)	8.19.1+dfsg-3	80.065,5 kB	339.636,0 kB	[Liste der Dateien]
ppc64el	8.20.0+dfsg-1+b1	69.085,0 kB	266.602,0 kB	[Liste der Dateien]
riscv64	8.20.0+dfsg-1+b1	69.428,3 kB	265.949,0 kB	[Liste der Dateien]
s390x	8.20.0+dfsg-1+b1	69.219,0 kB	274.470,0 kB	[Liste der Dateien]
sh4 (inoffizielle Portierung)	8.12.0-3+b3	103.401,4 kB	412.954,0 kB	[Liste der Dateien]
sparc64 (inoffizielle Portierung)	8.12.0-3+b3	103.374,8 kB	412.882,0 kB	[Liste der Dateien]
x32 (inoffizielle Portierung)	8.12.0-3+b3	103.397,8 kB	412.954,0 kB	[Liste der Dateien]