Autor:	Polonowski, Emmanuel
Rok vydání:	2012
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	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.
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1212.0253 Zobrazit plný text záznamu View this record from Arxiv