Pakiet: coq (8.16.1+dfsg-1 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: libc6 (>= 2.35)

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

• dep: libcoq-core-ocaml-4ew58 [armhf]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-7k9u9 [s390x]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-cpf60 [amd64]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-cqbo5 [ppc64el]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-cspq5 [i386]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-wc485 [arm64]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-stdlib (= 8.16.1+dfsg-1+b2)

  proof assistant for higher-order logic (theories)

• dep: libfindlib-ocaml-0thr1 [amd64]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-3yei3 [armhf]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-85sc9 [i386]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-9bk70 [ppc64el]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-dhcd7 [s390x]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-unji9 [arm64]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libgmp10 (>= 2:6.2.1+dfsg1)

  Biblioteka działań arytmetycznych z dużą dokładnością

• dep: libzarith-ocaml-4dps0 [amd64, arm64, ppc64el]

  pakiet wirtualny udostępniany przez libzarith-ocaml

• dep: libzarith-ocaml-aip06 [armhf, i386]

  pakiet wirtualny udostępniany przez libzarith-ocaml

• dep: libzarith-ocaml-vtl52 [s390x]

  pakiet wirtualny udostępniany przez libzarith-ocaml

• dep: ocaml-base-4.13.1

  pakiet wirtualny udostępniany przez ocaml-base

• dep: ocaml-findlib

  Narzędzie zarządzające bibliotekami OCaml

• dep: ocaml-nox

  transitional package for ocaml

• dep: python3

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

• 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-core-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
amd64	8.16.1+dfsg-1+b2	91 027,9 KiB	352 732,0 KiB	[lista plików]
arm64	8.16.1+dfsg-1+b2	99 773,5 KiB	398 315,0 KiB	[lista plików]
armhf	8.16.1+dfsg-1+b2	87 761,3 KiB	286 184,0 KiB	[lista plików]
i386	8.16.1+dfsg-1+b2	85 466,2 KiB	312 470,0 KiB	[lista plików]
ppc64el	8.16.1+dfsg-1+b2	91 686,3 KiB	372 982,0 KiB	[lista plików]
s390x	8.16.1+dfsg-1+b2	91 127,8 KiB	375 279,0 KiB	[lista plików]