如何有效地使用Agda的自动certificatesearch?

在写certificate时,我注意到Agda的自动certificatesearch经常找不到对我来说显而易见的解决scheme。 不幸的是想出了一个小例子,说明这个问题似乎很难,所以我试图描述最常见的模式。

  • 我忘了将-m添加到孔中以使Agda查看模块范围。 我可以将该标志设为默认值吗? 会有什么缺点?
  • 通常当前空洞可以由我将要实现的函数的参数填充。 即使添加-m ,Agda也不会考虑letwhere子句中引入的函数参数或符号。 简单地尝试所有这些,有什么不对吗?
  • 在查看目标时,甚至不显示letwhere子句中引入的符号。 为什么?

还有哪些其他习惯可以使自动更有效?

    Agda的自动校对search被硬编入编译器。 这使得速度更快,但限制了你可以做的定制量。 另一种方法是使用Agda的reflection机制来实施类似的certificatesearch程序。 使用TC monad最近的反思版本,你不再需要实现你自己的统一过程。

    Carlos Tome一直在重新实现这些想法(查看他的代码https://github.com/carlostome/AutoInAgda )。 他一直在努力尝试使用上下文信息,打印debugging信息等几个版本。希望这有助于!