|
|
|
Linux temps réel embarqué et outils de développements
|
Technique |
|
|
coq7-libs
| coq7-libs | proof assistant for higher-order logic (Coq 7 theories) | | Priority | |
| Section | math |
| 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. |
|
|
|
Etude RTOS