package rocq-metarocq-template

MetaRocq is a meta-programming framework for Rocq.

Template Rocq is a quoting library for Rocq. It takes Rocq terms and constructs a representation of their syntax tree as a Rocq 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 Rocq 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 MetaRocq/MTac.