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

[ Источник:  ]

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

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

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

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

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

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

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

• dep: libcoq-ocaml-4s3g2

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

• dep: libnum-ocaml-3st20

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

• dep: ocaml-base-nox-4.11.1

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

• dep: ocaml-findlib

  management tool for OCaml libraries

• dep: ocaml-nox

  transitional package for ocaml

• 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-ocaml-dev

  development libraries and tools for Coq

• sug: why (>= 2.19)

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

Загрузка coq

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

Архитектура	Версия	Размер пакета	В установленном виде	Файлы
alpha (неофициальный перенос)	8.12.0-3+b3	103 380,6 Кб	412 882,0 Кб	[список файлов]