Package: coq (8.16.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: libc6 (>= 2.35)

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

• dep: libcoq-core-ocaml-4ew58 [armhf]

  virtual package provided by libcoq-core-ocaml

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

  virtual package provided by libcoq-core-ocaml

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

  virtual package provided by libcoq-core-ocaml

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

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-core-ocaml-cspq5 [i386]

  virtual package provided by libcoq-core-ocaml

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

  virtual package provided by libcoq-core-ocaml

• dep: libcoq-stdlib (= 8.16.1+dfsg-1+b2)

  assistente alle dimostrazioni per logiche di ordine superiore (teorie)

• dep: libfindlib-ocaml-0thr1 [amd64]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-3yei3 [armhf]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-85sc9 [i386]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-9bk70 [ppc64el]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-dhcd7 [s390x]

  virtual package provided by libfindlib-ocaml

• dep: libfindlib-ocaml-unji9 [arm64]

  virtual package provided by libfindlib-ocaml

• dep: libgmp10 (>= 2:6.2.1+dfsg1)

  libreria aritmetica a precisione multipla

• dep: libzarith-ocaml-4dps0 [amd64, arm64, ppc64el]

  virtual package provided by libzarith-ocaml

• dep: libzarith-ocaml-aip06 [armhf, i386]

  virtual package provided by libzarith-ocaml

• dep: libzarith-ocaml-vtl52 [s390x]

  virtual package provided by libzarith-ocaml

• dep: ocaml-base-4.13.1

  virtual package provided by ocaml-base

• dep: ocaml-findlib

  strumento di gestione per librerie Ocaml

• dep: ocaml-nox

  pacchetto di transizione per ocaml

• dep: python3

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

• sug: coq-doc

  documentation for Coq

• sug: coqide

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

  or proofgeneral

  frontend generico per assistenti alla dimostrazione

• sug: ledit

  editor di riga per programmi interattivi

  or readline-editor

  virtual package provided by ledit, rlfe, rlwrap

• sug: libcoq-core-ocaml-dev

  librerie e strumenti di sviluppo per Coq

• sug: why (>= 2.19)

  Package not available

Download coq

Download for all available architectures

Architecture	Version	Package Size	Installed Size	Files
amd64	8.16.1+dfsg-1+b2	91,027.9 kB	352,732.0 kB	[list of files]
arm64	8.16.1+dfsg-1+b2	99,773.5 kB	398,315.0 kB	[list of files]
armhf	8.16.1+dfsg-1+b2	87,761.3 kB	286,184.0 kB	[list of files]
i386	8.16.1+dfsg-1+b2	85,466.2 kB	312,470.0 kB	[list of files]
ppc64el	8.16.1+dfsg-1+b2	91,686.3 kB	372,982.0 kB	[list of files]
s390x	8.16.1+dfsg-1+b2	91,127.8 kB	375,279.0 kB	[list of files]