パッケージ: coq (8.16.1+dfsg-1 など)

[ ソース: coq  ]

高階論理証明アシスタント (トップレベルおよびコンパイラ)

Coq は高階論理の証明アシスタントで、コンピュータプログラムを形式的な仕様との 整合性を保ちながら開発できます。Objective Caml と Camlp5 を用いて 開発されています。

本パッケージは Coq へのコマンドラインインターフェース coqtop を提供します。

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-4ew58 [armhf]

  以下のパッケージによって提供される仮想パッケージです: libcoq-core-ocaml

• dep: libcoq-core-ocaml-7k9u9 [s390x]

  以下のパッケージによって提供される仮想パッケージです: libcoq-core-ocaml

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

  以下のパッケージによって提供される仮想パッケージです: libcoq-core-ocaml

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

  以下のパッケージによって提供される仮想パッケージです: libcoq-core-ocaml

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

  以下のパッケージによって提供される仮想パッケージです: libcoq-core-ocaml

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

  以下のパッケージによって提供される仮想パッケージです: libcoq-core-ocaml

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

  高階論理用の証明アシスタント (理論)

• dep: libfindlib-ocaml-0thr1 [amd64]

  以下のパッケージによって提供される仮想パッケージです: libfindlib-ocaml

• dep: libfindlib-ocaml-3yei3 [armhf]

  以下のパッケージによって提供される仮想パッケージです: libfindlib-ocaml

• dep: libfindlib-ocaml-85sc9 [i386]

  以下のパッケージによって提供される仮想パッケージです: libfindlib-ocaml

• dep: libfindlib-ocaml-9bk70 [ppc64el]

  以下のパッケージによって提供される仮想パッケージです: libfindlib-ocaml

• dep: libfindlib-ocaml-dhcd7 [s390x]

  以下のパッケージによって提供される仮想パッケージです: libfindlib-ocaml

• dep: libfindlib-ocaml-unji9 [arm64]

  以下のパッケージによって提供される仮想パッケージです: libfindlib-ocaml

• dep: libgmp10 (>= 2:6.2.1+dfsg1)

  多倍長精度演算ライブラリ

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

  以下のパッケージによって提供される仮想パッケージです: libzarith-ocaml

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

  以下のパッケージによって提供される仮想パッケージです: libzarith-ocaml

• dep: libzarith-ocaml-vtl52 [s390x]

  以下のパッケージによって提供される仮想パッケージです: libzarith-ocaml

• dep: ocaml-base-4.13.1

  以下のパッケージによって提供される仮想パッケージです: ocaml-base

• 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

  高階論理用証明アシスタント (gtk インターフェイス)

  または proofgeneral

  証明アシスタント用の汎用フロントエンド

• sug: ledit

  対話的プログラム向けのラインエディタ

  または readline-editor

  以下のパッケージによって提供される仮想パッケージです: ledit, rlfe, rlwrap

• sug: libcoq-core-ocaml-dev

  development libraries and tools for Coq

• sug: why (>= 2.19)

  パッケージは利用できません

coq のダウンロード

すべての利用可能アーキテクチャ向けのダウンロード

アーキテクチャ	バージョン	パッケージサイズ	インストールサイズ	ファイル
amd64	8.16.1+dfsg-1+b2	91,027.9 kB	352,732.0 kB	[ファイル一覧]
arm64	8.16.1+dfsg-1+b2	99,773.5 kB	398,315.0 kB	[ファイル一覧]
armhf	8.16.1+dfsg-1+b2	87,761.3 kB	286,184.0 kB	[ファイル一覧]
i386	8.16.1+dfsg-1+b2	85,466.2 kB	312,470.0 kB	[ファイル一覧]
ppc64el	8.16.1+dfsg-1+b2	91,686.3 kB	372,982.0 kB	[ファイル一覧]
s390x	8.16.1+dfsg-1+b2	91,127.8 kB	375,279.0 kB	[ファイル一覧]