Paquet : coq (8.19.1+dfsg-1)

Liens pour coq

Ressources Debian :

Télécharger le paquet source coq :

Responsables :

Ressources externes :

Page d'accueil [coq.inria.fr]

Paquets similaires :

outil d'aide à la preuve pour la logique d'ordre supérieur (environnement interactif et compilateur)

Coq est un assistant de preuve pour la logique d'ordre supérieur, qui permet le développement de programmes d'ordinateur correspondant à une spécification formelle. Il est développé en Objective Caml et Camlp5.

Ce paquet fournit coqtop, une interface en ligne de commande pour Coq.

Une interface graphique pour Coq est fournie dans le paquet coqide. On peut aussi utiliser Coq avec ProofGeneral, qui permet l'édition de preuves dans Emacs et XEmacs. Pour cela, le paquet proofgeneral doit être installé.

É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

dépendances

recommandations

suggestions

enhances

dep: libc6 (>= 2.35)

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

paquet virtuel fourni par libcoq-core-ocaml
dep: libcoq-stdlib (= 8.19.1+dfsg-1)

outil d'aide à la preuve pour la logique d'ordre supérieur (théories)
dep: libfindlib-ocaml-449z9

paquet virtuel fourni par libfindlib-ocaml
dep: libgmp10 (>= 2:6.3.0+dfsg)

Bibliothèque arithmétique à multi-précision
dep: libstdlib-ocaml-ep7y0

paquet virtuel fourni par libstdlib-ocaml
dep: libzarith-ocaml-zlfv4

paquet virtuel fourni par libzarith-ocaml
dep: ocaml

mise en oeuvre de Meta Language avec un système orienté objet basé sur les classes
dep: ocaml-base-4.14.1

paquet virtuel fourni par ocaml-base
dep: ocaml-findlib

management tool for OCaml libraries
dep: python3

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

sug: coq-doc

documentation for Coq
sug: coqide

outil d'aide à la preuve pour la logique d'ordre supérieur (interface en GTK)

ou proofgeneral

frontal générique d’assistants de preuve
sug: ledit

éditeur de lignes pour les programmes interactifs

ou readline-editor

paquet virtuel fourni par ledit, rlfe, rlwrap
sug: libcoq-core-ocaml-dev

development libraries and tools for Coq
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	80 224,7 ko	306 550,0 ko	[liste des fichiers]