English

DBGen User Manual

Logic in Computer Science 2012-12-04 v1

Abstract

DBGen is a tool for Coq developers. It takes as input the definition of a term structure with bindings annotations and generates definitions and properties for lifting and substitution in the De Bruijn setting, up to the substitution lemma. It provides also a named syntax and a translation function to the De Bruijn syntax.

Cite

@article{arxiv.1212.0253,
  title  = {DBGen User Manual},
  author = {Emmanuel Polonowski},
  journal= {arXiv preprint arXiv:1212.0253},
  year   = {2012}
}
R2 v1 2026-06-21T22:47:34.568Z