In this work, we present a visualisation tool that is able to process Coq proof scripts and generate a table representation of the contained proofs as $\LaTeX$ or PDF files. This tool has the aim to support both education and review processes as all proof steps can be visualised. Thus, there is no need to use Coq in order to review proofs or use them as examples in teaching. In contrast to the usual approach of visualising proofs as hypertext or markdown documents, the generated files can be easily printed.
翻译:在此工作中, 我们提出了一个可视化工具, 可以处理 Coq 校验脚本, 并生成包含的校验表格, 以$\\ LaTeX$ 或 PDF 文件表示 。 此工具的目的是支持教育和审查过程, 因为所有校验步骤都可以直观化。 因此, 没有必要使用 Coq 来审查校验或作为教学范例。 与通常将校验作为超文本或标记文件的可视化方法相比, 生成的文件可以很容易地打印 。