找出哪些元素在Agda程序中未解决

找出导致未解析元素的原因的最佳方法是什么？有没有办法通过扩展所有可解的通配符来将所有未解析的元素（只有未解析的元素）变成漏洞？找出哪些元素在Agda程序中未解决

如果没有别的办法，是否将未解决的元素更改为洞使关于未解析元的消息消失？因为那么我想我可以尝试将每个通配符和每个隐含的参数都改为孔，直到消息消失，然后找出哪一个导致问题...

2012-04-21 Cactus

我加了一个Haskell的标签，因为阿格达标签具有唯一的17个问题 – sdcvvc 2012-04-26 21:42:48

在这种情况下，让我改变标题也是如此 - 如果你认为这是关于这个问题的话哈斯克尔，你只会感到困惑... – Cactus 2012-04-27 07:25:09

一种方法（不一定是最好的）是替换所有隐论点明确下划线：

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

2012-07-16 13:52:46 xrchz

那么这是否意味着从第二段我的问题的积极答案？ “把一个未解决的元变成一个洞会使有关未解决元的消息消失吗？” – Cactus 2012-07-19 06:26:53

回答