package coq-metacoq
A meta-programming framework for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.2-8.17.tar.gz
sha512=a5ce2f5d94120a00703331a3cfdb7d51653fb44adeba89fa84b5f76e711ee9f582a22551f81fd144dc974e3f05e58d85cd716f8fcf69ec89923bc64774d82668
Description
MetaCoq is a meta-programming framework for Coq.
The meta-package includes the template-coq library, the PCUIC development including a verified equivalence between Coq and PCUIC, a safe type checker and verified erasure for PCUIC and example translations.
See individual packages for more detailed descriptions.
Published: 22 Apr 2023
Dependencies (4)
-
coq-metacoq-quotation
= version
-
coq-metacoq-translations
= version
-
coq-metacoq-erasure-plugin
= version
-
coq-metacoq-safechecker-plugin
= version
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)" x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)">
On This Page