Пакет: coq (8.18.0+dfsg-1)

[ Источник: coq  ]

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

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

• dep: libc6 (>= 2.35)

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

• dep: libcoq-core-ocaml-fg9y1 [amd64]

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

• dep: libcoq-core-ocaml-jwuq2 [i386]

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

• dep: libcoq-core-ocaml-lsl44 [s390x]

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

• dep: libcoq-core-ocaml-ru4g2 [armhf]

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

• dep: libcoq-core-ocaml-t2nr4 [arm64]

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

• dep: libcoq-core-ocaml-zchk9 [ppc64el]

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

• dep: libcoq-stdlib (= 8.18.0+dfsg-1)

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

• dep: libfindlib-ocaml-449z9 [amd64]

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

• dep: libfindlib-ocaml-9adu2 [armhf]

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

• dep: libfindlib-ocaml-goqu1 [i386]

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

• dep: libfindlib-ocaml-ift94 [arm64]

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

• dep: libfindlib-ocaml-k3zo5 [s390x]

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

• dep: libfindlib-ocaml-z40n4 [ppc64el]

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

• dep: libgmp10 (>= 2:6.3.0+dfsg)

  библиотека для работы с числами произвольной точности

• dep: libstdlib-ocaml-058x2 [ppc64el]

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

• dep: libstdlib-ocaml-dkl58 [i386]

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

• dep: libstdlib-ocaml-ep7y0 [amd64]

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

• dep: libstdlib-ocaml-fyga0 [arm64]

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

• dep: libstdlib-ocaml-rayz1 [armhf]

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

• dep: libstdlib-ocaml-vneg5 [s390x]

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

• dep: libzarith-ocaml-avzf2 [s390x]

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

• dep: libzarith-ocaml-wx6x8 [armhf, i386]

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

• dep: libzarith-ocaml-zlfv4 [amd64, arm64, ppc64el]

  виртуальный пакет, предоставляемый 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

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

Архитектура	Размер пакета	В установленном виде	Файлы
amd64	79 803,6 Кб	304 414,0 Кб	[список файлов]
arm64	86 045,9 Кб	339 767,0 Кб	[список файлов]
armhf	76 577,9 Кб	254 297,0 Кб	[список файлов]
i386	75 346,2 Кб	274 242,0 Кб	[список файлов]
ppc64el	79 779,9 Кб	319 989,0 Кб	[список файлов]
s390x	79 310,7 Кб	320 633,0 Кб	[список файлов]