软件包：coq（8.9.0-1）

[ 源代码： coq  ]

proof assistant for higher-order logic (toplevel and compiler)

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

This package provides coqtop, a command line interface to Coq.

The proofgeneral package allows proofs to be edited using Emacs and XEmacs.

标签: 软件开发: 编译器, 领域: 数学, 实做语言: implemented-in::ocaml, interface::commandline, 用户接口: 文本模式, 角色: role::program, scope::utility, 界面工具箱: Ncurses TUI

其他与 coq 有关的软件包

• dep: coq-theories (= 8.9.0-1)

  proof assistant for higher-order logic (theories)

• dep: libc6 (>= 2.28)

  GNU C 语言运行库：共享库
  同时作为一个虚包由这些包填实： libc6-udeb

• dep: libcoq-ocaml-fl0a8

  本虚包由这些包填实： libcoq-ocaml

• dep: ocaml-base-nox-4.05.0

  本虚包由这些包填实： ocaml-base-nox

• dep: ocaml-findlib

  management tool for OCaml libraries

• dep: ocaml-nox

  ML implementation with a class-based object system (no X)

• dep: python3

  交互式高级面向对象语言（默认 python3 版本）

• sug: coq-doc

  软件包暂时不可用

• sug: ledit

  line editor for interactive programs

  或者 readline-editor

  本虚包由这些包填实： ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: proofgeneral

  软件包暂时不可用

• sug: why (>= 2.19)

  软件包暂时不可用

下载 coq

下载可用于所有硬件架构的

硬件架构	软件包大小	安装后大小	文件
armhf	55,983.5 kB	197,337.0 kB	[文件列表]