パッケージ: coq (8.12.0-3 など)

[ ソース: 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: coq-theories (= 8.12.0-3+b3)

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

• dep: libc6 (>= 2.29) [armel, mips64el, mipsel 以外]

  GNU C ライブラリ: 共有ライブラリ
  以下のパッケージによって提供される仮想パッケージでもあります: libc6-udeb

• dep: libcoq-ocaml-1fwg6 [ppc64el]

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

• dep: libcoq-ocaml-4pem8 [arm64]

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

• dep: libcoq-ocaml-4s3g2 [armel, mips64el, mipsel]

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

• dep: libcoq-ocaml-otko2 [i386]

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

• dep: libcoq-ocaml-xs455 [amd64]

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

• dep: libcoq-ocaml-zuzr9 [armhf]

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

• dep: libnum-ocaml-3st20 [armel, mips64el, mipsel]

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

• dep: libnum-ocaml-80ki3 [amd64, arm64, ppc64el]

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

• dep: libnum-ocaml-hqq52 [armhf, i386]

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

• dep: ocaml-base-nox-4.11.1

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

• dep: ocaml-findlib

  management tool for OCaml libraries

• dep: ocaml-nox

  クラスベースのオブジェクトシステムを持った ML 言語の実装

• dep: python3

  対話式の高レベルオブジェクト指向言語 (デフォルト python3 バージョン)

• sug: coq-doc

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

• sug: coqide

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

  または proofgeneral

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

• sug: ledit

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

  または readline-editor

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

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: why (>= 2.19)

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

coq のダウンロード

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

アーキテクチャ	バージョン	パッケージサイズ	インストールサイズ	ファイル
amd64	8.12.0-3+b3	88,333.2 kB	358,108.0 kB	[ファイル一覧]
arm64	8.12.0-3+b3	93,820.2 kB	384,451.0 kB	[ファイル一覧]
armel	8.12.0-3+b3	103,391.0 kB	412,954.0 kB	[ファイル一覧]
armhf	8.12.0-3+b3	86,284.5 kB	308,733.0 kB	[ファイル一覧]
i386	8.12.0-3+b3	85,826.4 kB	329,208.0 kB	[ファイル一覧]
mips64el	8.12.0-3+b3	103,385.3 kB	412,882.0 kB	[ファイル一覧]
mipsel	8.12.0-3+b3	103,402.0 kB	412,954.0 kB	[ファイル一覧]
ppc64el	8.12.0-3+b3	89,332.1 kB	371,137.0 kB	[ファイル一覧]