Пакет: coq (8.18.0+dfsg-1 и другие)

Ссылки для 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: libc6 (>= 2.35)

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

виртуальный пакет, предоставляемый libcoq-core-ocaml
dep: libcoq-stdlib (= 8.18.0+dfsg-1+b1)

интерактивное программное средство доказательства теорем логики высшего порядка (теории)
dep: libfindlib-ocaml-goqu1

виртуальный пакет, предоставляемый libfindlib-ocaml
dep: libgmp10 (>= 2:6.3.0+dfsg)

библиотека для работы с числами произвольной точности
dep: libstdlib-ocaml-dkl58

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

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

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

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

management tool for OCaml libraries
dep: python3

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

sug: coq-doc

documentation for Coq
sug: coqide

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

или proofgeneral

generic frontend for proof assistants
sug: ledit

line editor for interactive programs

или readline-editor

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

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

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

Загрузка coq

Загрузить для всех доступных архитектур
Архитектура	Версия	Размер пакета	В установленном виде	Файлы
i386	8.18.0+dfsg-1+b1	75 346,1 Кб	274 243,0 Кб	[список файлов]