|
|
|
Linux temps réel embarqué et outils de développements
|
Technique |
|
|
coq-libs
| coq-libs | proof assistant for higher-order logic (theories) | | Priority | |
| Section | math |
| Installed size | 6800 |
| 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/coq-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 that new proofs can be based upon, including theories of arithmetic and Boolean values. |
|
|
|
Etude RTOS