Paket: coq (9.1.0+dfsg-1)

Länkar för coq

Debianresurser:

Hämta källkodspaketet coq:

Ansvariga:

Debian OCaml Maintainers (QA-sida, E-postarkiv)
Benjamin Barenblat (QA-sida)
Julien Puydt (QA-sida)
Ralf Treinen (QA-sida)
Stéphane Glondu (QA-sida)

Externa resurser:

Hemsida [coq.inria.fr]

Liknande paket:

Experimentellt paket

Varning: Paketet är från den experimentella utgåvan. Det innebär att det med stor sannolikhet är instabilt eller innehåller fel, och kanske till och med kan orsaka dataförluster. Se till att läsa ändringsloggen och annan dokumentation innan du använder det.

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.

A graphical interface for Coq is provided in the coqide package. Coq can also be used with ProofGeneral, which allows proofs to be edited using emacs and xemacs. This requires the proofgeneral package to be installed.

Märken: Software Development: Compiler, Field: Matematik, Implemented in: implemented-in::ocaml, interface::commandline, User Interface: Text-based Interactive, Role: role::program, scope::utility, Interface Toolkit: Ncurses TUI

Andra paket besläktade med coq

beror

rekommenderar

föreslår

enhances

dep: libc6 (>= 2.38)

GNU C-bibliotek: Delade bibliotek
också ett virtuellt paket som tillhandahålls av libc6-udeb
dep: libcoq-core (= 9.1.0+dfsg-1)

proof assistant for higher-order logic (theories)
dep: libcoq-core-ocaml-3d0o2 [ppc64el]

virtuellt paket som tillhandahålls av libcoq-core-ocaml
dep: libcoq-core-ocaml-501i1 [s390x]

virtuellt paket som tillhandahålls av libcoq-core-ocaml
dep: libcoq-core-ocaml-qojm9 [arm64]

virtuellt paket som tillhandahålls av libcoq-core-ocaml
dep: libcoq-core-ocaml-rqof7 [amd64]

virtuellt paket som tillhandahålls av libcoq-core-ocaml
dep: libfindlib-ocaml-8k3o3 [amd64]

Paketet inte tillgängligt
dep: libfindlib-ocaml-itlb4 [ppc64el]

Paketet inte tillgängligt
dep: libfindlib-ocaml-svhk3 [s390x]

Paketet inte tillgängligt
dep: libfindlib-ocaml-vaiw6 [arm64]

Paketet inte tillgängligt
dep: libgmp10 (>= 2:6.3.0+dfsg)

Multiprecision arithmetic library
dep: libstdlib-ocaml-2d5j3 [s390x]

Paketet inte tillgängligt
dep: libstdlib-ocaml-m4xw9 [ej s390x]

Paketet inte tillgängligt
dep: libzarith-ocaml-2ofb9 [s390x]

Paketet inte tillgängligt
dep: libzarith-ocaml-h79v1 [ej s390x]

Paketet inte tillgängligt
dep: ocaml

ML language implementation with a class-based object system
dep: ocaml-base-5.3.0

Paketet inte tillgängligt
dep: ocaml-findlib

management tool for OCaml libraries
dep: python3

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

sug: coq-doc

documentation for Coq
sug: ledit

line editor for interactive programs

eller readline-editor

Paketet inte tillgängligt
sug: libcoq-core-ocaml-dev

development libraries and tools for Coq
sug: rocqide

proof assistant for higher-order logic (gtk interface)

eller proofgeneral

generic frontend for proof assistants
sug: why (>= 2.19)

Paketet inte tillgängligt

Hämta coq

Hämtningar för alla tillgängliga arkitekturer
Arkitektur	Paketstorlek	Installerad storlek	Filer
amd64	38.679,5 kbyte	160.187,0 kbyte	[filförteckning]
arm64	42.220,8 kbyte	178.262,0 kbyte	[filförteckning]
ppc64el	39.383,1 kbyte	169.751,0 kbyte	[filförteckning]
s390x	39.313,2 kbyte	175.585,0 kbyte	[filförteckning]