摘要：初学者面临的一个主要障碍是Isabelle/HOL要求所有定义在使用之前都必须声明，而（互相）递归的定义必须同时定义。本文中，我们描述了这个问题的解决方案，这将使初学者以及真实模型更容易使用翻译插件。
作者：Leo Freitas
论文ID：2304.15006
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-01
PDF 下载： 英文版 中文版pdf翻译中