Paquet : coq-theories (8.12.0-3 et autres) [debports]

[ Paquet source :  ]

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

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 contient des théories existantes sur lesquelles les nouvelles preuves peuvent se baser, incluant des théories arithmétiques et des valeurs booléennes.

Autres paquets associés à coq-theories

• dep: coq-8.12.0+4.11.1

  paquet virtuel fourni par coq

• rec: coq (>= 8.0)

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

Télécharger coq-theories

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

Architecture	Version	Taille du paquet	Espace occupé une fois installé	Fichiers
alpha (portage non officiel)	8.12.0-3+b3	23 361,0 ko	166 285,0 ko	[liste des fichiers]
hppa (portage non officiel)	8.12.0-3+b3	23 358,5 ko	166 204,0 ko	[liste des fichiers]
ia64 (portage non officiel)	8.12.0-3+b3	23 359,0 ko	166 286,0 ko	[liste des fichiers]
sh4 (portage non officiel)	8.12.0-3+b3	23 351,6 ko	166 203,0 ko	[liste des fichiers]
sparc64 (portage non officiel)	8.12.0-3+b3	23 359,8 ko	166 286,0 ko	[liste des fichiers]
x32 (portage non officiel)	8.12.0-3+b3	23 356,3 ko	166 203,0 ko	[liste des fichiers]