Pakiet: coq (8.20.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: coq-libs (= 8.1.pl3+dfsg-1) [m68k]

  Pakiet niedostępny

• dep: coq-theories (= 8.12.0-3+b3) [alpha, hppa, ia64, sh4, sparc64, x32]

  proof assistant for higher-order logic (theories)

• dep: emacsen-common [m68k]

  Wspólne udogodnienie dla wszystkich pakietów emacs

• dep: libc6 (>= 2.38) [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

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

  dep: libc6 (>= 2.39) [loong64]

  dep: libc6 (>= 2.5-5) [m68k]

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

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

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

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

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

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-d2hd1 [loong64]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

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

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-t2147 [riscv64]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-core-ocaml-yi844 [ppc64]

  pakiet wirtualny udostępniany przez libcoq-core-ocaml

• dep: libcoq-ocaml-4s3g2 [alpha, hppa, ia64, sh4, sparc64, x32]

  pakiet wirtualny udostępniany przez libcoq-ocaml

• dep: libcoq-stdlib (= 8.19.1+dfsg-3) [loong64, ppc64]

  proof assistant for higher-order logic (theories)

  dep: libcoq-stdlib (= 8.20.1+dfsg-1) [amd64, arm64, ppc64el, riscv64, s390x]

• dep: libfindlib-ocaml-5dit4 [arm64]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-9a346 [s390x]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-l8hb7 [ppc64]

  Pakiet niedostępny

• dep: libfindlib-ocaml-o8mp7 [ppc64el]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-t0ap1 [loong64]

  Pakiet niedostępny

• dep: libfindlib-ocaml-t4zk4 [riscv64]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libfindlib-ocaml-xdxk1 [amd64]

  pakiet wirtualny udostępniany przez libfindlib-ocaml

• dep: libgmp10 (>= 2:6.3.0+dfsg) [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]

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

• dep: libncurses5 (>= 5.6+20071006-3) [m68k]

  Pakiet niedostępny

• dep: libnum-ocaml-3st20 [alpha, hppa, ia64, sh4, sparc64, x32]

  pakiet wirtualny udostępniany przez libnum-ocaml

• dep: libstdlib-ocaml-fxjy5 [amd64, arm64, ppc64el, riscv64]

  pakiet wirtualny udostępniany przez libstdlib-ocaml

• dep: libstdlib-ocaml-gats1 [ppc64]

  Pakiet niedostępny

• dep: libstdlib-ocaml-ke4j9 [s390x]

  pakiet wirtualny udostępniany przez libstdlib-ocaml

• dep: libstdlib-ocaml-vyp69 [loong64]

  Pakiet niedostępny

• dep: libzarith-ocaml-avzf2 [ppc64]

  Pakiet niedostępny

• dep: libzarith-ocaml-f1se9 [amd64, arm64, ppc64el, riscv64]

  pakiet wirtualny udostępniany przez libzarith-ocaml

• dep: libzarith-ocaml-i2hh0 [s390x]

  pakiet wirtualny udostępniany przez libzarith-ocaml

• dep: libzarith-ocaml-zlfv4 [loong64]

  Pakiet niedostępny

• dep: ocaml [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]

  Implementacja języka ML z systemem obiektowym bazującym na klasach

• dep: ocaml-base-4.14.1 [loong64, ppc64]

  pakiet wirtualny udostępniany przez ocaml-base

• dep: ocaml-base-5.3.0 [amd64, arm64, ppc64el, riscv64, s390x]

  pakiet wirtualny udostępniany przez ocaml-base

• dep: ocaml-base-nox-3.10.2 [m68k]

  Pakiet niedostępny

• dep: ocaml-base-nox-4.11.1 [alpha, hppa, ia64, sh4, sparc64, x32]

  Pakiet niedostępny

• dep: ocaml-findlib [nie m68k]

  Narzędzie zarządzające bibliotekami OCaml

• dep: ocaml-nox [alpha, hppa, ia64, sh4, sparc64, x32]

  Pakiet przejściowy do ocaml

• dep: python3 [nie m68k]

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

• dep: tex-common (>= 1.10) [m68k]

  Wspólna infrastruktura do budowy i instalacji systemu TeX

• rec: coqide

  proof assistant for higher-order logic (gtk interface)

  lub proofgeneral-coq

  Pakiet niedostępny

• sug: cle [m68k]

  Pakiet niedostępny

• sug: coq-doc

  documentation for Coq

• sug: coqide [nie m68k]

  proof assistant for higher-order logic (gtk interface)

  lub proofgeneral

  Ogólny interfejs dla asystentów dowodzenia twierdzeń

• sug: ledit [m68k]

  line editor for interactive programs

• sug: ledit [nie m68k]

  line editor for interactive programs

  lub readline-editor

  pakiet wirtualny udostępniany przez ledit, rlfe, rlwrap

• sug: libcoq-core-ocaml-dev [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]

  development libraries and tools for Coq

• sug: libcoq-ocaml-dev [alpha, hppa, ia64, sh4, sparc64, x32]

  development libraries and tools for Coq

• sug: ocaml-nox (>= 3.08) [m68k]

  Pakiet przejściowy do ocaml

• sug: proofgeneral-coq [m68k]

  Pakiet niedostępny

• sug: why (>= 2.19) [nie m68k]

  Pakiet niedostępny

Pobieranie coq

Pobierz dla wszystkich dostępnych architektur

Architektura	Wersja	Rozmiar pakietu	Rozmiar po instalacji	Pliki
alpha (port nieoficjalny)	8.12.0-3+b3	103 380,6 KiB	412 882,0 KiB	[lista plików]
amd64	8.20.1+dfsg-1	68 574,8 KiB	255 831,0 KiB	[lista plików]
arm64	8.20.1+dfsg-1	72 692,7 KiB	277 363,0 KiB	[lista plików]
hppa (port nieoficjalny)	8.12.0-3+b3	103 393,2 KiB	412 952,0 KiB	[lista plików]
ia64 (port nieoficjalny)	8.12.0-3+b3	103 379,1 KiB	412 878,0 KiB	[lista plików]
loong64 (port nieoficjalny)	8.19.1+dfsg-3	82 879,7 KiB	330 249,0 KiB	[lista plików]
m68k (port nieoficjalny)	8.1.pl3+dfsg-1+b2	4 014,9 KiB	18 580,0 KiB	[lista plików]
ppc64 (port nieoficjalny)	8.19.1+dfsg-3	80 065,5 KiB	339 636,0 KiB	[lista plików]
ppc64el	8.20.1+dfsg-1	69 187,4 KiB	266 936,0 KiB	[lista plików]
riscv64	8.20.1+dfsg-1	69 527,1 KiB	266 346,0 KiB	[lista plików]
s390x	8.20.1+dfsg-1	69 405,7 KiB	274 877,0 KiB	[lista plików]
sh4 (port nieoficjalny)	8.12.0-3+b3	103 401,4 KiB	412 954,0 KiB	[lista plików]
sparc64 (port nieoficjalny)	8.12.0-3+b3	103 374,8 KiB	412 882,0 KiB	[lista plików]
x32 (port nieoficjalny)	8.12.0-3+b3	103 397,8 KiB	412 954,0 KiB	[lista plików]