package coq-template-coq

  1. Overview
  2. No Docs
A quoting and unquoting library for Coq in Coq

Install

Dune Dependency

template-coq.github.io Edit opam file Versions (2)

Authors

  1. A
    Abhishek Anand <aa755@cs.cornell.edu>
  2. S
    Simon Boulier <simon.boulier@inria.fr>
  3. C
    Cyril Cohen <cyril.cohen@inria.fr>
  4. G
    Gregory Malecha <gmalecha@gmail.com>
  5. M
    Matthieu Sozeau <matthieu.sozeau@inria.fr>
  6. N
    Nicolas Tabareau <nicolas.tabareau@inria.fr>

Maintainers

  1. M
    matthieu.sozeau@inria.fr

Sources

v2.1-beta3.tar.gz
md5=e81b8ecabef788a10337a39b095d54f3

Description

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.

Published: 14 Aug 2018

Dependencies (2)

  1. coq >= "8.8" & < "8.9~"
  2. ocaml >= "4.05"

Dev Dependencies

None

Used by (1)

  1. coq-switch < "1.0.1"

Conflicts

None