package coq-metacoq-safechecker
Implementation and verification of safe conversion and typechecking algorithms for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
v1.1.1-8.15.tar.gz
sha512=83d6b109217139640a081a9ef98b35cf33b1f568b8941f0b23d43abd25d22331cee16fbdd77335583fe74fea0f28215facf1cd9cb416e460a785c6061a454bae
Description
MetaCoq is a meta-programming framework for Coq.
The SafeChecker modules provides a correct implementation of weak-head reduction, conversion and typechecking of Coq definitions and global environments.
Published: 12 Oct 2022
Dependencies (1)
-
coq-metacoq-pcuic
= version
Dev Dependencies
None
Used by (2)
-
coq-metacoq
= "1.1.1+8.15" -
coq-metacoq-erasure
= "1.1.1+8.15"
Conflicts
None
On This Page