Pakiet: coq (8.12.0-3 i inne) [debports]
Odnośniki dla coq
Zasoby systemu Debian:
Pobieranie pakietu źródłowego :
Nie znalezionoOpiekunowie:
Zasoby zewnętrzne:
- Strona internetowa [coq.inria.fr]
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.
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 niedostępny
-
- dep: ocaml-findlib
- Narzędzie zarządzające bibliotekami OCaml
-
- dep: ocaml-nox
- transitional package for ocaml
-
- dep: python3
- Interaktywny, wysokopoziomowy i obiektowy język programowania (domyślna wersja Python 3)
-
- sug: coq-doc
- documentation for Coq
-
- 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
| Architektura | Wersja | Rozmiar pakietu | Rozmiar po instalacji | Pliki |
|---|---|---|---|---|
| x32 (port nieoficjalny) | 8.12.0-3+b3 | 103 397,8 KiB | 412 954,0 KiB | [lista plików] |