Pakiet: coq (8.9.0-1)

[ Pakiet źródłowy: 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.

Znaczniki: Rozwój oprogramowania: Kompilator, Dziedzina: Matematyka, Zaimplementowane w: implemented-in::ocaml, interface::commandline, Interfejs użytkownika: Interaktywny interfejs tekstowy, Rola: role::program, scope::utility, Pakiet narzędziowy interfejsu: Ncurses (terminalowy)

Inne pakiety związane z coq

• dep: coq-theories (= 8.9.0-1)

  proof assistant for higher-order logic (theories)

• dep: libc6 (>= 2.28)

  Biblioteka GNU C: biblioteki współdzielone
  również pakiet wirtualny udostępniany przez libc6-udeb

• dep: libcoq-ocaml-fl0a8

  pakiet wirtualny udostępniany przez libcoq-ocaml

• dep: ocaml-base-nox-4.05.0

  pakiet wirtualny udostępniany przez ocaml-base-nox

• dep: ocaml-findlib

  Narzędzie zarządzające bibliotekami OCaml

• dep: ocaml-nox

  Implementacja ML z systemem obiektowym bazującym na klasach (nie do X-ów)

• dep: python3

  Interaktywny, wysokopoziomowy i obiektowy język programowania (domyślna wersja Python 3)

• sug: coq-doc

  Pakiet niedostępny

• sug: ledit

  line editor for interactive programs

  lub readline-editor

  pakiet wirtualny udostępniany przez ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: proofgeneral

  Pakiet niedostępny

• sug: why (>= 2.19)

  Pakiet niedostępny

Pobieranie coq

Pobierz dla wszystkich dostępnych architektur

Architektura	Rozmiar pakietu	Rozmiar po instalacji	Pliki
armhf	55 983,5 KiB	197 337,0 KiB	[lista plików]