Paket: coq (8.9.0-1)

[ Quellcode: coq  ]

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.

The proofgeneral package allows proofs to be edited using Emacs and XEmacs.

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-theories (= 8.9.0-1)

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

• dep: libc6 (>= 2.28)

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

• dep: libcoq-ocaml-35sv0

  virtuelles Paket, bereitgestellt durch libcoq-ocaml

• dep: ocaml-base-nox-4.05.0

  virtuelles Paket, bereitgestellt durch ocaml-base-nox

• dep: ocaml-findlib

  Verwaltungswerkzeug für OCaml-Bibliotheken

• dep: ocaml-nox

  ML-Implementierung mit einem klassenbasierten Objektsystem (ohne X)

• dep: python3

  Interaktive objektorientierte Hochsprache (Python3-Standardversion)

• sug: coq-doc

  Paket nicht verfügbar

• sug: ledit

  Zeileneditor für interaktive Programme

  oder readline-editor

  virtuelles Paket, bereitgestellt durch ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: proofgeneral

  Paket nicht verfügbar

• sug: why (>= 2.19)

  Paket nicht verfügbar

coq herunterladen

Download für alle verfügbaren Architekturen

Architektur	Paketgröße	Größe (installiert)	Dateien
i386	54.878,8 kB	208.963,0 kB	[Liste der Dateien]