Пакунок: coq (8.12.0-3 and others) [debports]

[ Source:  ]

Інтерактивний програмний засіб доведення теорем для логіки вищого порядку (інтерактивне середовище і компілятор)

Coq — допоміжний інструмент для доведення теорем логіки вищого порядку, що дозволяє розробляти комп'ютерні програми відповідно до їх формальної специфікації. Ця програма написана на Objective Caml та Camlp5.

Пакунок надає „coqtop“, інтерфейс командного рядка для Coq.

Графічний інтерфейс Coq надається пакунком „coqide“. Coq також може використовуватися з ProofGeneral, який дозволяє редагувати докази в „emacs“ та „xemacs“. Останнє вимагає встановлення пакунка „proofgeneral“.

Інші пакунки пов'язані з coq

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

  proof assistant for higher-order logic (theories)

• dep: libcoq-ocaml-4s3g2

  virtual package provided by libcoq-ocaml

• dep: libnum-ocaml-3st20

  virtual package provided by 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

  interactive high-level object-oriented language (default python3 version)

• sug: coq-doc

  documentation for Coq

• sug: coqide

  proof assistant for higher-order logic (gtk interface)

  or proofgeneral

  generic frontend for proof assistants

• sug: ledit

  line editor for interactive programs

  or readline-editor

  virtual package provided by ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: why (>= 2.19)

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

Завантажити coq

Завантаження для всіх доступних архітектур

Архітектура	Версія	Розмір пакунка	Розмір після встановлення	Файли
ia64 (unofficial port)	8.12.0-3+b3	103,379.1 kB	412,878.0 kB	[список файлів]