Пакет: coq (8.12.0-3 и другие)

Ссылки для coq

Ресурсы Debian:

Исходный код coq:

Сопровождающие:

Внешние ресурсы:

Сайт [coq.inria.fr]

Подобные пакеты:

интерактивное программное средство доказательства теорем для логики высшего порядка (интерактивная среда и компилятор)

Coq — вспомогательный инструмент для доказательства теорем логики высшего порядка, позволяющий разрабатывать компьютерные программы в соответствии с их формальной спецификацией. Эта программа написана на Objective Caml и Camlp5.

Пакет предоставляет coqtop, интерфейс командной строки для Coq.

Графический интерфейс Coq предоставляется пакетом coqide. Coq также может использоваться с ProofGeneral, который позволяет редактировать доказательства в emacs и xemacs. Последнее требует установки пакета proofgeneral.

Теги: Разработка программного обеспечения: Компилятор, Область: Математика, Реализовано на: implemented-in::ocaml, interface::commandline, Пользовательский интерфейс: Интерактивный, на основе вводимого текста, Роль: role::program, scope::utility, Инструментарий интерфейса: Ncurses TUI

Другие пакеты, относящиеся к coq

зависимости

рекомендации

предложения

enhances

dep: coq-theories (= 8.12.0-3+b3)

интерактивное программное средство доказательства теорем логики высшего порядка (теории)
dep: libc6 (>= 2.29) [не armel, mips64el, mipsel]

библиотека GNU C: динамически подключаемые библиотеки
также виртуальный пакет, предоставляемый libc6-udeb
dep: libcoq-ocaml-1fwg6 [ppc64el]

виртуальный пакет, предоставляемый libcoq-ocaml
dep: libcoq-ocaml-4pem8 [arm64]

виртуальный пакет, предоставляемый libcoq-ocaml
dep: libcoq-ocaml-4s3g2 [armel, mips64el, mipsel]

виртуальный пакет, предоставляемый libcoq-ocaml
dep: libcoq-ocaml-otko2 [i386]

виртуальный пакет, предоставляемый libcoq-ocaml
dep: libcoq-ocaml-xs455 [amd64]

виртуальный пакет, предоставляемый libcoq-ocaml
dep: libcoq-ocaml-zuzr9 [armhf]

виртуальный пакет, предоставляемый libcoq-ocaml
dep: libnum-ocaml-3st20 [armel, mips64el, mipsel]

виртуальный пакет, предоставляемый libnum-ocaml
dep: libnum-ocaml-80ki3 [amd64, arm64, ppc64el]

виртуальный пакет, предоставляемый libnum-ocaml
dep: libnum-ocaml-hqq52 [armhf, i386]

виртуальный пакет, предоставляемый libnum-ocaml
dep: ocaml-base-nox-4.11.1

виртуальный пакет, предоставляемый ocaml-base-nox
dep: ocaml-findlib

management tool for OCaml libraries
dep: ocaml-nox

реализация языка ML с объектной системой на основе классов (без зависимостей от X)
dep: python3

интерактивный высокоуровневый объектно-ориентированный язык (версия python3 по умолчанию)

sug: coq-doc

Пакет недоступен
sug: coqide

интерактивное программное средство доказательства теорем логики высшего порядка (интерфейс GTK)

или proofgeneral

generic frontend for proof assistants
sug: ledit

line editor for interactive programs

или readline-editor

виртуальный пакет, предоставляемый ledit, rlfe, rlwrap
sug: libcoq-ocaml-dev

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

Пакет недоступен

Загрузка coq

Загрузить для всех доступных архитектур
Архитектура	Версия	Размер пакета	В установленном виде	Файлы
amd64	8.12.0-3+b3	88 333,2 Кб	358 108,0 Кб	[список файлов]
arm64	8.12.0-3+b3	93 820,2 Кб	384 451,0 Кб	[список файлов]
armel	8.12.0-3+b3	103 391,0 Кб	412 954,0 Кб	[список файлов]
armhf	8.12.0-3+b3	86 284,5 Кб	308 733,0 Кб	[список файлов]
i386	8.12.0-3+b3	85 826,4 Кб	329 208,0 Кб	[список файлов]
mips64el	8.12.0-3+b3	103 385,3 Кб	412 882,0 Кб	[список файлов]
mipsel	8.12.0-3+b3	103 402,0 Кб	412 954,0 Кб	[список файлов]
ppc64el	8.12.0-3+b3	89 332,1 Кб	371 137,0 Кб	[список файлов]