Pakiet: coq (8.12.0-3 i inne)

[ Pakiet źródłowy: coq  ]

Asystent udowadniania logiki wyższego rzędu (interfejs i kompilator)

Coq jest asystentem udowadniania nadrzędnej logiki, która pozwala na rozwój programów komputerowych zgodnych z ich oficjalną specyfikacją. Został opracowany przy użyciu Objective Caml i Camlp5.

Pakiet zawiera coqtop, interfejs wiersza poleceń do Coq.

Graficzny interfejs do Coq znajduje się w pakiecie coqide. Coq można również stosować z ProofGeneral, który umożliwia edytowanie dowodów przy użyciu emacs i xemacs. W tym celu należy zainstalować pakiet proofgeneral.

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.12.0-3+b3)

  proof assistant for higher-order logic (theories)

• dep: libcoq-ocaml-4s3g2

  pakiet wirtualny udostępniany przez libcoq-ocaml

• dep: libnum-ocaml-3st20

  pakiet wirtualny udostępniany przez libnum-ocaml

• dep: ocaml-base-nox-4.11.1

  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

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

• sug: coq-doc

  Pakiet niedostępny

• sug: coqide

  proof assistant for higher-order logic (gtk interface)

  lub proofgeneral

  Ogólny interfejs dla asystentów dowodzenia twierdzeń

• 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: why (>= 2.19)

  Pakiet niedostępny

Pobieranie coq

Pobierz dla wszystkich dostępnych architektur

Architektura	Wersja	Rozmiar pakietu	Rozmiar po instalacji	Pliki
armel	8.12.0-3+b3	103 391,0 KiB	412 954,0 KiB	[lista plików]