找出导致未解决的元数据的最佳方法是什么?有没有办法通过扩展所有可解决的周围通配符将所有未解决的元数据(并且只有未解决的元数据)变成孔?
如果不出意外,将未解决的元数据更改为漏洞是否会使有关未解决的元数据的消息消失?因为那时我想我可以尝试将每个通配符和每个隐式参数都更改为漏洞,直到消息消失,然后找出导致问题的原因...
找出导致未解决的元数据的最佳方法是什么?有没有办法通过扩展所有可解决的周围通配符将所有未解决的元数据(并且只有未解决的元数据)变成孔?
如果不出意外,将未解决的元数据更改为漏洞是否会使有关未解决的元数据的消息消失?因为那时我想我可以尝试将每个通配符和每个隐式参数都更改为漏洞,直到消息消失,然后找出导致问题的原因...
一种方法(不一定是最好的)是用显式下划线替换所有隐式参数:
f {_} {_} {_} (x {_} {_} {_})
此答案来自 Agda 邮件列表:https ://lists.chalmers.se/pipermail/agda/2012/004123.html