Пакет: coq (8.1.pl3+dfsg-1 и другие) [debports]

[ Источник:  ]

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 Camlp4. For more information, see <http://coq.inria.fr/>.

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

A graphical interface for Coq is provided in the coqide package. Coq can also be used with ProofGeneral, which allows proofs to be edited using emacs and xemacs. This requires the proofgeneral-coq package to be installed.

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

• dep: coq-libs (= 8.1.pl3+dfsg-1)

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

• dep: emacsen-common

  общие средства для всех пакетов emacs

• dep: libc6 (>= 2.5-5)

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

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

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

• dep: ocaml-base-nox-3.10.2

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

• dep: tex-common (>= 1.10)

  инфраструктура для сборки и установки TeX

• rec: coqide

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

  или proofgeneral-coq

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

• sug: cle

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

• sug: coq-doc

  documentation for Coq

• sug: ledit

  line editor for interactive programs

• sug: ocaml-nox (>= 3.08)

  transitional package for ocaml

• sug: proofgeneral-coq

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

Загрузка coq

Загрузить для всех доступных архитектур

Архитектура	Версия	Размер пакета	В установленном виде	Файлы
m68k (неофициальный перенос)	8.1.pl3+dfsg-1+b2	4 014,9 Кб	18 580,0 Кб	[список файлов]