找出哪些元素在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

回答