4
4

1 回答 1

6

这是在没有看到整个发展的情况下在黑暗中拍摄的镜头，但有时，当您看不到差异时，这意味着您看不到的部分存在差异。即，隐式参数。

例如，您可能在某处有一个隐式参数，该参数在工作证明尝试中的两个位置出现相同，并且在非工作证明尝试中出现在两个不同但可相互转换（甚至只是相等）的位置。有时策略需要相同的术语来触发，而可互换的术语对于相同的证明树就足够了，而相等的术语对于明智的引入就足够了eq_refl。当您使用高级策略（例如 setoid 策略）时，可能很难理解幕后发生的事情。

尝试比较Set Printing Implicitor下的情况Set Printing All，或者使用No Strict ImplicitorNo Implicit Arguments进行一小部分证明。

于 2011-11-15T08:17:34.740 回答