Package: coq (8.12.0-3 and others) [debports]

[ Source:  ]

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.

Other Packages Related to coq

• dep: coq-theories (= 8.12.0-3+b3)

  assistente alle dimostrazioni per logiche di ordine superiore (teorie)

• dep: libcoq-ocaml-4s3g2

  virtual package provided by libcoq-ocaml

• dep: libnum-ocaml-3st20

  virtual package provided by libnum-ocaml

• dep: ocaml-base-nox-4.11.1

  Package not available

• dep: ocaml-findlib

  strumento di gestione per librerie Ocaml

• dep: ocaml-nox

  pacchetto di transizione per ocaml

• dep: python3

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

• 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-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
ia64 (unofficial port)	8.12.0-3+b3	103,379.1 kB	412,878.0 kB	[list of files]