在编写校样时,我注意到Agda的自动校对搜索经常找不到对我来说显而易见的解决方案.不幸的是,提出一个小例子,说明问题似乎很难,所以我试着描述最常见的模式.
-m到孔中以使Agda查看模块范围.我可以将该标志设为默认值吗？会有什么缺点？-m,Agda也不会考虑在let或where子句中引入的函数参数或符号.简单地尝试所有这些都有问题吗？let或where子句中引入的符号.为什么？使用auto更有效的其他习惯是什么？
小智 1
Agda 的自动证明搜索被硬连线到编译器中。这使得速度更快，但限制了您可以进行的定制量。一种替代方法是使用 Agda 的反射机制来实现类似的证明搜索过程。通过最近使用 TC monad 的增强版反射，您不再需要实现自己的统一过程。
Carlos Tome 一直致力于重新实现这些想法（查看他的代码 https://github.com/carlostome/AutoInAgda）。他一直在开发多个版本，尝试使用上下文中的信息、打印调试信息等。希望这会有所帮助！