At the heart of most formal developments are inductive definitions, ranging from simple data structures to complex operational semantics of programming languages. We are developing InducTeX, a MetaCoq plugin for typesetting Coq inductives as inference rules with TeX.

The tool provides a convenient way of documenting and communicating inductive definitions, even to those who are not proficient in Coq. Furthermore, it saves authors from duplicating their Coq inference rules in TeX and having to keep them in sync with the corresponding Coq definitions.