找出在Agda程序中未解决的元数据

Question

最好的方式是找出未解决元的原因是什么？是否有一种方法可以通过扩展所有可解决的周围通配符，将所有未解决的元（仅限未解决的元）转换为洞？

如果没有其他办法，将未解决的元变成洞会使未解决元的消息消失吗？因为那样的话，我可以尝试将每个通配符和每个隐式参数变成洞，直到消息消失，然后找出哪一个是引起问题的...

- Cactus

Answer 1

一种方法（不一定是最好的）是将所有隐含的参数替换为显式的下划线：

f {_} {_} {_} (x {_} {_} {_})

这篇回答来自Agda邮件列表：https://lists.chalmers.se/pipermail/agda/2012/004123.html

（注：Agda是一种依赖类型的函数式编程语言，用于证明理论和程序开发）

- xrchz

---

那么这是否意味着对于我在第二段提出的问题的肯定回答呢？“将未解决的元转换为洞是否会使有关未解决的元的消息消失？” - Cactus

是的：漏洞在技术上是未解决的元问题，但被报告为漏洞。 - gallais