Package: coq (8.20.1+dfsg-1 and others)

[ Source: coq  ]

assistente alle dimostrazioni per logiche di ordine superiore (toplevel e compilatore)

Coq è un assistente alle dimostrazioni per logiche di ordine superiore che permette lo sviluppo di programmi per computer coerenti con la loro specifica formale. È sviluppato con Objective Caml e Camlp5.

Questo pacchetto fornisce coqtop, un'interfaccia a riga di comando per Coq.

Un'interfaccia grafica per Coq è inclusa nel pacchetto coqide. Coq può anche essere usato con ProofGeneral, che permette di modificare le dimostrazioni con emacs e xemacs. Quest'operazione richiede che sia installato il pacchetto proofgeneral.

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

Other Packages Related to coq

• dep: coq-libs (= 8.1.pl3+dfsg-1) [m68k]

  Package not available

• dep: coq-theories (= 8.12.0-3+b3) [alpha, hppa, ia64, sh4, sparc64, x32]

  assistente alle dimostrazioni per logiche di ordine superiore (teorie)

• dep: emacsen-common [m68k]

  funzionalità comuni per tutti gli emacs

• dep: libc6 (>= 2.38) [amd64, arm64, ppc64, ppc64el, riscv64, s390x]

  Libreria C GNU: librerie condivise
  also a virtual package provided by libc6-udeb

  dep: libc6 (>= 2.39) [loong64]

  dep: libc6 (>= 2.5-5) [m68k]

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

  virtual package provided by libcoq-core-ocaml

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

  virtual package provided by libcoq-core-ocaml

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

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-d2hd1 [loong64]

  virtual package provided by libcoq-core-ocaml

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

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-t2147 [riscv64]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-yi844 [ppc64]

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-ocaml-4s3g2 [alpha, hppa, ia64, sh4, sparc64, x32]

  virtual package provided by libcoq-ocaml

• dep: libcoq-stdlib (= 8.19.1+dfsg-3) [loong64, ppc64]

  assistente alle dimostrazioni per logiche di ordine superiore (teorie)

  dep: libcoq-stdlib (= 8.20.1+dfsg-1) [amd64, arm64, ppc64el, riscv64, s390x]

• dep: libfindlib-ocaml-5dit4 [arm64]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-9a346 [s390x]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-l8hb7 [ppc64]

  Package not available

• dep: libfindlib-ocaml-o8mp7 [ppc64el]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-t0ap1 [loong64]

  Package not available

• dep: libfindlib-ocaml-t4zk4 [riscv64]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-xdxk1 [amd64]

  virtual package provided by libfindlib-ocaml

• dep: libgmp10 (>= 2:6.3.0+dfsg) [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]

  libreria aritmetica a precisione multipla

• dep: libncurses5 (>= 5.6+20071006-3) [m68k]

  Package not available

• dep: libnum-ocaml-3st20 [alpha, hppa, ia64, sh4, sparc64, x32]

  virtual package provided by libnum-ocaml

• dep: libstdlib-ocaml-fxjy5 [amd64, arm64, ppc64el, riscv64]

  virtual package provided by libstdlib-ocaml

• dep: libstdlib-ocaml-gats1 [ppc64]

  Package not available

• dep: libstdlib-ocaml-ke4j9 [s390x]

  virtual package provided by libstdlib-ocaml

• dep: libstdlib-ocaml-vyp69 [loong64]

  Package not available

• dep: libzarith-ocaml-avzf2 [ppc64]

  Package not available

• dep: libzarith-ocaml-f1se9 [amd64, arm64, ppc64el, riscv64]

  virtual package provided by libzarith-ocaml

• dep: libzarith-ocaml-i2hh0 [s390x]

  virtual package provided by libzarith-ocaml

• dep: libzarith-ocaml-zlfv4 [loong64]

  Package not available

• dep: ocaml [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]

  implementazione del linguaggio ML con un sistema basato su classi e oggetti

• dep: ocaml-base-4.14.1 [loong64, ppc64]

  virtual package provided by ocaml-base

• dep: ocaml-base-5.3.0 [amd64, arm64, ppc64el, riscv64, s390x]

  virtual package provided by ocaml-base

• dep: ocaml-base-nox-3.10.2 [m68k]

  Package not available

• dep: ocaml-base-nox-4.11.1 [alpha, hppa, ia64, sh4, sparc64, x32]

  Package not available

• dep: ocaml-findlib [not m68k]

  strumento di gestione per librerie Ocaml

• dep: ocaml-nox [alpha, hppa, ia64, sh4, sparc64, x32]

  pacchetto di transizione per ocaml

• dep: python3 [not m68k]

  linguaggio interattivo di alto livello orientato agli oggetti (versione python3 predefinita)

• dep: tex-common (>= 1.10) [m68k]

  infrastruttura comune per compilare e installare TeX

• rec: coqide

  assistente alle dimostrazioni per logiche di ordine superiore (interfaccia gtk)

  or proofgeneral-coq

  Package not available

• sug: cle [m68k]

  Package not available

• sug: coq-doc

  documentation for Coq

• sug: coqide [not m68k]

  assistente alle dimostrazioni per logiche di ordine superiore (interfaccia gtk)

  or proofgeneral

  frontend generico per assistenti alla dimostrazione

• sug: ledit [m68k]

  editor di riga per programmi interattivi

• sug: ledit [not m68k]

  editor di riga per programmi interattivi

  or readline-editor

  virtual package provided by ledit, rlfe, rlwrap

• sug: libcoq-core-ocaml-dev [amd64, arm64, loong64, ppc64, ppc64el, riscv64, s390x]

  librerie e strumenti di sviluppo per Coq

• sug: libcoq-ocaml-dev [alpha, hppa, ia64, sh4, sparc64, x32]

  librerie e strumenti di sviluppo per Coq

• sug: ocaml-nox (>= 3.08) [m68k]

  pacchetto di transizione per ocaml

• sug: proofgeneral-coq [m68k]

  Package not available

• sug: why (>= 2.19) [not m68k]

  Package not available

Download coq

Download for all available architectures

Architecture	Version	Package Size	Installed Size	Files
alpha (unofficial port)	8.12.0-3+b3	103,380.6 kB	412,882.0 kB	[list of files]
amd64	8.20.1+dfsg-1	68,574.8 kB	255,831.0 kB	[list of files]
arm64	8.20.1+dfsg-1	72,692.7 kB	277,363.0 kB	[list of files]
hppa (unofficial port)	8.12.0-3+b3	103,393.2 kB	412,952.0 kB	[list of files]
ia64 (unofficial port)	8.12.0-3+b3	103,379.1 kB	412,878.0 kB	[list of files]
loong64 (unofficial port)	8.19.1+dfsg-3	82,879.7 kB	330,249.0 kB	[list of files]
m68k (unofficial port)	8.1.pl3+dfsg-1+b2	4,014.9 kB	18,580.0 kB	[list of files]
ppc64 (unofficial port)	8.19.1+dfsg-3	80,065.5 kB	339,636.0 kB	[list of files]
ppc64el	8.20.1+dfsg-1	69,187.4 kB	266,936.0 kB	[list of files]
riscv64	8.20.1+dfsg-1	69,527.1 kB	266,346.0 kB	[list of files]
s390x	8.20.1+dfsg-1	69,405.7 kB	274,877.0 kB	[list of files]
sh4 (unofficial port)	8.12.0-3+b3	103,401.4 kB	412,954.0 kB	[list of files]
sparc64 (unofficial port)	8.12.0-3+b3	103,374.8 kB	412,882.0 kB	[list of files]
x32 (unofficial port)	8.12.0-3+b3	103,397.8 kB	412,954.0 kB	[list of files]