我目前正在寻找一种从一些依赖类型语言（可能是 Coq）中的归纳定义生成 LaTeX 推理规则（水平线样式）的方法。
我找到了这个包，但它看起来很脆弱，没有很多最近的更新，并且每当它遇到 unicode 时都会默默地失败。
我想知道的是，我可以滥用 Coq 在 OCaml 中编写 Tactics 来检查Inductive定义并将其格式化为 LaTeX 的能力吗？显然我会自己编写格式化代码，但我想知道如何获得 AST 表示
这里和这里有一些插件介绍教程，但它们只提供基础知识，而且我还没有找到插件 API 的真正文档，所以我不确定如何获得归纳类型的 OCaml 表示，例如，类型的名称，或该类型的目标。
这已经完成了吗？是否有现有的工具可以做到这一点，或者类似的东西，我可以用作例子吗？