Balík: coq (8.20.1+dfsg-1 a iné)

Odkazy pre coq

Zdroje Debian:

Stiahnuť zdrojový balík coq:

Správcovia:

Externé zdroje:

Domovská stránka [coq.inria.fr]

Podobné balíky:

asistent dôkazov logiky vyššieho rádu (najvyššia úroveň a kompilátor)

Coq je asistent dôkazov logiky vyššieho rádu, ktorý umožňuje vývoj počítačových programov v súlade s ich formálnou špecifikáciou. Bol vyvinutý pomocou Objective Caml a Camlp5.

Tento balík poskytuje coqtop, rozhranie príkazového riadka ku Coq.

Grafické rozhranie ku Coq poskytuje balík coqide. Coq je tiež možné používať spolu s ProofGeneral, ktorý umožňuje upravovanie dôkazov pomocou emacs a xemacs. To vyžaduje, aby bol nainštalovaný balík proofgeneral.

Značky: Software Development: Kompilátor, Pole: Matematika, Implementované v: implemented-in::ocaml, interface::commandline, User Interface: Text-based Interactive, Role: role::program, scope::utility, Sada nástrojov používateľského rozhrania: Ncurses TUI

Ostatné balíky súvisiace s balíkom coq

závisí

odporúča

navrhuje

vylepšuje

dep: libc6 (>= 2.38)

knižnica GNU C - zdieľané knižnice
tiež virtuálny balík poskytovaný balíkom libc6-udeb
dep: libcoq-core-ocaml-29kh7 [amd64]

virtuálny balík poskytovaný balíkom libcoq-core-ocaml
dep: libcoq-core-ocaml-cm0q5 [s390x]

virtuálny balík poskytovaný balíkom libcoq-core-ocaml
dep: libcoq-core-ocaml-n64h2 [ppc64el]

virtuálny balík poskytovaný balíkom libcoq-core-ocaml
dep: libcoq-core-ocaml-rho03 [riscv64]

virtuálny balík poskytovaný balíkom libcoq-core-ocaml
dep: libcoq-core-ocaml-ub9d2 [arm64]

virtuálny balík poskytovaný balíkom libcoq-core-ocaml
dep: libcoq-stdlib (= 8.20.1+dfsg-1+b1)

asistent dôkazov logiky vyššieho rádu (teórie)
dep: libfindlib-ocaml-8k3o3 [amd64]

virtuálny balík poskytovaný balíkom libfindlib-ocaml
dep: libfindlib-ocaml-eitb4 [riscv64]

virtuálny balík poskytovaný balíkom libfindlib-ocaml
dep: libfindlib-ocaml-itlb4 [ppc64el]

virtuálny balík poskytovaný balíkom libfindlib-ocaml
dep: libfindlib-ocaml-svhk3 [s390x]

virtuálny balík poskytovaný balíkom libfindlib-ocaml
dep: libfindlib-ocaml-vaiw6 [arm64]

virtuálny balík poskytovaný balíkom libfindlib-ocaml
dep: libgmp10 (>= 2:6.3.0+dfsg)

aritmetická knižnica s viacnásobnou presnosťou
dep: libstdlib-ocaml-2d5j3 [s390x]

virtuálny balík poskytovaný balíkom libstdlib-ocaml
dep: libstdlib-ocaml-m4xw9 [nie s390x]

virtuálny balík poskytovaný balíkom libstdlib-ocaml
dep: libzarith-ocaml-2ofb9 [s390x]

virtuálny balík poskytovaný balíkom libzarith-ocaml
dep: libzarith-ocaml-h79v1 [nie s390x]

virtuálny balík poskytovaný balíkom libzarith-ocaml
dep: ocaml

ML language implementation with a class-based object system
dep: ocaml-base-5.3.0

virtuálny balík poskytovaný balíkom ocaml-base
dep: ocaml-findlib

nástroj na správu knižníc OCaml
dep: python3

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

sug: coq-doc

documentation for Coq
sug: coqide

asistent dôkazov logiky vyššieho rádu (rozhranie GTK)

alebo proofgeneral

generic frontend for proof assistants
sug: ledit

riadkový editor pre interaktívne programy

alebo readline-editor

virtuálny balík poskytovaný balíkom ledit, rlfe, rlwrap
sug: libcoq-core-ocaml-dev

development libraries and tools for Coq
sug: why (>= 2.19)

Balík nie je dostupný

Stiahnuť coq

Stiahnuť pre všetky dostupné architektúry
Architektúra	Verzia	Veľkosť balíka	Nainštalovaná veľkosť	Súbory
amd64	8.20.1+dfsg-1+b1	68,576.4 kB	255,832.0 kB	[zoznam súborov]
arm64	8.20.1+dfsg-1+b1	72,701.2 kB	277,428.0 kB	[zoznam súborov]
ppc64el	8.20.1+dfsg-1+b1	69,193.7 kB	266,937.0 kB	[zoznam súborov]
riscv64	8.20.1+dfsg-1+b1	69,526.1 kB	266,347.0 kB	[zoznam súborov]
s390x	8.20.1+dfsg-1+b1	69,370.3 kB	274,882.0 kB	[zoznam súborov]