ott:Ott工具，用于编写编程语言和计算的定义

奥特 Ott是用于编写编程语言和计算的定义的工具。 它以一种简明易读的ASCII表示法作为一种语言语法和语义的定义的输入，该表示法与人们在非正式数学中所写的内容非常接近。 使用适当的注释，它然后可以生成输出： LaTeX源文件，该文件定义了用于定义定义的排版版本的命令； 定义的Coq版本； 定义的HOL版本； 该定义的Isabelle / HOL版本； 定义的Lem版本； 定义语法的OCaml版本； 和 （实验性的）竖竖式语法分析器和语法的简明漂亮打印机。 另外，它可以作为过滤器运行，获取带有定义语言的嵌入式（符号）术语的LaTeX / Coq / Isabelle / HOL / Lem / OCaml源文件，对其进行解析并将其替换为排版术语。 最简单的是，Ott可用于辅助非正式的LaTeX数学。 在这里，它允许以清晰，可编辑的ASCII表示法来编写证明和说明中的定义以及