coq-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, runable as a plugin. - Example plugins built on top of this.

opam install coq-template-coq.2.0~beta
homepage
https://template-coq.github.io/template-coq
license
MIT
bugs tracker
https://github.com/Template-Coq/template-coq/issues
dependencies
coq (>= 8.7 & < 8.8~)
source
https://github.com/Template-Coq/template-coq/archive/v2.0-beta.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-template-coq/coq-template-coq.2.0~beta