Linux temps réel embarqué et outils de développements Technique


coq7-libs proof assistant for higher-order logic (Coq 7 theories)
Installed size 6984
Maintainer Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Architecture all
Version 8.0pl3-2
Depends libc6 (>= 2.3.5-1), libncurses5 (>= 5.4-5), coq-libs (= 8.0pl3-2)
Suggests ocaml-nox (>= 3.08), proofgeneral-coq, ledit, cle
File name pool/main/c/coq/coq7-libs_8.0pl3-2_all.deb
Description 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 Camlp4. For more information, see http://coq.inria.fr/. . This package provides existing theories from Coq 7 in Coq 8, and allows proofs that were developed in Coq 7 to be used in Coq 8. It is also required to translate theories in Coq 7 syntax into the new syntax introduced in Coq 8. However, this package does not need to be installed to use Coq 7.

©M.N.I.S Société | Produits | Services | Formations | Support | Partenariat | Presse | Téléchargements ©M.N.I.S