Пакет: coq (8.9.0-1)

Ссылки для coq

Ресурсы Debian:

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

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

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

Сайт [coq.inria.fr]

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

proof assistant for higher-order logic (toplevel and compiler)

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

This package provides coqtop, a command line interface to Coq.

The proofgeneral package allows proofs to be edited using Emacs and XEmacs.

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

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

зависимости

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

предложения

enhances

dep: coq-theories (= 8.9.0-1)

интерактивное программное средство доказательства теорем логики высшего порядка (теории)
dep: libc6 (>= 2.28)

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

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

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

management tool for OCaml libraries
dep: ocaml-nox

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

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

sug: coq-doc

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

line editor for interactive programs

или readline-editor

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

development libraries and tools for Coq
sug: proofgeneral

Пакет недоступен
sug: why (>= 2.19)

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

Загрузка coq

Загрузить для всех доступных архитектур
Архитектура	Размер пакета	В установленном виде	Файлы
amd64	57 608,0 Кб	233 951,0 Кб	[список файлов]