wszystkie opcje
buster  ] [  bullseye  ] [  bookworm  ] [  trixie  ] [  sid  ]
[ Pakiet źródłowy: coq  ]

Pakiet: coq (8.16.1+dfsg-1 i inne)

Odnośniki dla coq

Screenshot

Zasoby systemu Debian:

Pobieranie pakietu źródłowego coq:

Opiekunowie:

Zasoby zewnętrzne:

Podobne pakiety:

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

  • wymaga
  • poleca
  • sugeruje
  • enhances

Pobieranie coq

Pobierz dla wszystkich dostępnych architektur
Architektura Wersja Rozmiar pakietu Rozmiar po instalacji Pliki
s390x 8.16.1+dfsg-1+b2 91 127,8 KiB375 279,0 KiB [lista plików]