[  etch  ] [  etch-m68k  ] [  lenny  ] [  squeeze  ] [  sid  ]
[ Source: coq  ]

Package: coq (8.1.pl3+dfsg-1 and others)

Dokazovací nástroj vyšší logiky (nejvyšší úroveň a kompilátor)

Coq je dokazovací asistent logiky vyššího řádu, který umožňuje vývoj počítačových programů konzistentních s jejich formálními specifikacemi. Je vyvíjen pomocí objektového Caml a Camlp4. Pro více informací se podívejte na <http://coq.inria.fr/>.

Tento balíček obsahuje coqtop, rozhraní příkazové řádky k Coq.

Grafické rozhraní Coq je obsaženo v balíčku coqide. Coq také používá ProofGeneral, který umožní úpravu důkazů pomocí editoru emacs a xemacs. To vyžaduje instalaci balíčku proofgeneral-coq.

Tags: Software Development: Compiler, Field: Mathematics, Implemented in: OCaml, User Interface: Command Line, Text-based Interactive, Role: Program, Scope: Utility, Interface Toolkit: Ncurses TUI

Other Packages Related to coq

  • depends
  • recommends
  • suggests
  • dep: coq-libs (= 8.1.pl3+dfsg-1)
    Asistent dokazovací logiky vyššího řádu (teorie)
  • dep: emacsen-common
    Společné příslušenství pro všechny emacsy
  • dep: libc6 (>= 2.7-1) [not alpha, ia64]
    Knihovna GNU C: Sdílené knihovny
    also a virtual package provided by libc6-udeb
  • dep: libc6.1 (>= 2.7-1) [alpha, ia64]
    Knihovna GNU C: Sdílené knihovny
    also a virtual package provided by libc6.1-udeb
  • dep: libgcc1 (>= 1:4.3) [armel]
    Knihovna pro překladač GCC
  • dep: libncurses5 (>= 5.6+20071006-3)
    Sdílené knihovny pro obsluhu terminálu
  • dep: ocaml-base-nox-3.10.2
    virtual package provided by ocaml-base-nox
  • dep: tex-common (>= 1.10)
    common infrastructure for building and installing TeX
  • rec: coqide
    Dokazovací asistent používající logiku vyššího řádu (s rozhraním gtk)
    or proofgeneral-coq
    generic interface for proof assistants - coq support
  • sug: cle
    Zachytí jakýkoliv příkaz příkazové řádky pomocí readline
  • sug: coq-doc
    documentation for Coq in html format
  • sug: ledit
    Řádkový editor pro interaktivní programy
  • sug: ocaml-nox (>= 3.08)
    ML language implementation with a class-based object system
  • sug: proofgeneral-coq
    generic interface for proof assistants - coq support

Download coq

Download for all available architectures
Architecture Version Package Size Installed Size Files
alpha 8.1.pl3+dfsg-1+b2 4,238.4 kB19404 kB [list of files]
amd64 8.1.pl3+dfsg-1+b2 8,825.9 kB33696 kB [list of files]
arm 8.1.pl3+dfsg-1+b2 4,091.6 kB18804 kB [list of files]
armel 8.1.pl3+dfsg-1+b2 4,116.3 kB18864 kB [list of files]
hppa 8.1.pl3+dfsg-1+b2 4,180.0 kB18988 kB [list of files]
i386 8.1.pl3+dfsg-1+b2 8,264.1 kB30272 kB [list of files]
ia64 8.1.pl3+dfsg-1+b2 4,370.6 kB20380 kB [list of files]
mips 8.1.pl3+dfsg-1+b2 4,145.0 kB19336 kB [list of files]
mipsel 8.1.pl3+dfsg-1+b2 4,132.1 kB19316 kB [list of files]
powerpc 8.1.pl3+dfsg-1+b2 9,236.7 kB32096 kB [list of files]
s390 8.1.pl3+dfsg-1+b2 4,226.0 kB19076 kB [list of files]
sparc 8.1.pl3+dfsg-1+b2 9,245.7 kB32372 kB [list of files]