Coq OPAMcoq-template-coq
A quoting and unquoting library for Coq in Coq. Template Coq is a quoting library for Coq. It takes Coq terms and constructs a representation of their syntax tree as a Coq inductive data type. The representation is based on the kernel's term representation. In addition to a complete reification and denotation of CIC terms, Template Coq includes: - Reification of the environment structures, for constant and inductive declarations. - Denotation of terms and global declarations - A monad for manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MetaCoq/MTac. - A partial type-checker for the Calculus of Inductive Constructions, runnable as a plugin. - Example plugins built on top of this.
opam install coq-template-coq.2.1~beta3
- homepage
- https://template-coq.github.io/template-coq
- license
- MIT
- bugs tracker
- https://github.com/Template-Coq/template-coq/issues
- dependencies
- coq (>= 8.8 & < 8.9~)
- source
- https://github.com/MetaCoq/metacoq/archive/v2.1-beta3.tar.gz
- package
- https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-template-coq/coq-template-coq.2.1~beta3