Information for RPM coq-8.18.0-4.fc40.src.rpm
ID | 1254204 | |||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Name | coq | |||||||||||||||||||||||
Version | 8.18.0 | |||||||||||||||||||||||
Release | 4.fc40 | |||||||||||||||||||||||
Epoch | ||||||||||||||||||||||||
Arch | src | |||||||||||||||||||||||
Summary | Proof management system | |||||||||||||||||||||||
Description | Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages (e.g. the CompCert compiler certification project, or the Bedrock verified low-level programming library), the formalization of mathematics (e.g. the full formalization of the Feit-Thompson theorem or homotopy type theory) and teaching. | |||||||||||||||||||||||
Build Time | 2024-03-20 05:33:35 GMT | |||||||||||||||||||||||
Size | 7.30 MB | |||||||||||||||||||||||
17a07840bb64928f91694933d3854a1a | ||||||||||||||||||||||||
License | LGPL-2.1-only AND MIT AND BSD-3-Clause | |||||||||||||||||||||||
Buildroot | f40-build-793211-138784 | |||||||||||||||||||||||
Provides |
|
|||||||||||||||||||||||
Obsoletes | No Obsoletes | |||||||||||||||||||||||
Conflicts | No Conflicts | |||||||||||||||||||||||
Requires |
|
|||||||||||||||||||||||
Recommends | No Recommends | |||||||||||||||||||||||
Suggests | No Suggests | |||||||||||||||||||||||
Supplements | No Supplements | |||||||||||||||||||||||
Enhances | No Enhances | |||||||||||||||||||||||
Files |
|
|||||||||||||||||||||||
Component of | No Buildroots |