Paquet : coq (8.9.0-1)

[ Paquet source : coq  ]

proof assistant for higher-order logic (toplevel and compiler)

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

This package provides coqtop, a command line interface to Coq.

The proofgeneral package allows proofs to be edited using Emacs and XEmacs.

Étiquettes: Développement de logiciel: Compilateur, Domaine: Mathématiques, Mis en œuvre en: implemented-in::ocaml, interface::commandline, Interface utilisateur: Interactive en mode texte, Rôle: role::program, scope::utility, Boîte à outils d'interface utilisateur: Interface utilisateur texte ncurses

Autres paquets associés à coq

• dep: coq-theories (= 8.9.0-1)

  outil d'aide à la preuve pour la logique d'ordre supérieur (théories)

• dep: libc6 (>= 2.28)

  bibliothèque C GNU : bibliothèques partagées
  un paquet virtuel est également fourni par libc6-udeb

• dep: libcoq-ocaml-m8xw4

  paquet virtuel fourni par libcoq-ocaml

• dep: ocaml-base-nox-4.05.0

  paquet virtuel fourni par ocaml-base-nox

• dep: ocaml-findlib

  management tool for OCaml libraries

• dep: ocaml-nox

  mise en œuvre de Meta Language avec un système orienté objet (pas de X)

• dep: python3

  langage orienté objet interactif de haut niveau – version par défaut de Python 3

• sug: coq-doc

  Paquet indisponible

• sug: ledit

  éditeur de lignes pour les programmes interactifs

  ou readline-editor

  paquet virtuel fourni par ledit, rlfe, rlwrap

• sug: libcoq-ocaml-dev

  development libraries and tools for Coq

• sug: proofgeneral

  Paquet indisponible

• sug: why (>= 2.19)

  Paquet indisponible

Télécharger coq

Télécharger pour toutes les architectures proposées

Architecture	Taille du paquet	Espace occupé une fois installé	Fichiers
amd64	57 608,0 ko	233 951,0 ko	[liste des fichiers]