Package: coq (8.9.0-1)

[ 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.

Il pacchetto proofgeneral permette di modificare le dimostrazioni con Emacs e XEmacs.

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-theories (= 8.9.0-1)

  assistente alle dimostrazioni per logiche di ordine superiore (teorie)

• dep: libc6 (>= 2.28)

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

• dep: libcoq-ocaml-yvk13

  virtual package provided by libcoq-ocaml

• dep: ocaml-base-nox-4.05.0

  virtual package provided by ocaml-base-nox

• dep: ocaml-findlib

  strumento di gestione per librerie Ocaml

• dep: ocaml-nox

  implementazione di ML con sistema a oggetti basato su classi (senza X)

• dep: python3

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

• sug: coq-doc

  Package not available

• 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: proofgeneral

  Package not available

• sug: why (>= 2.19)

  Package not available

Download coq

Download for all available architectures

Architecture	Package Size	Installed Size	Files
arm64	61,852.8 kB	254,534.0 kB	[list of files]