使用帶有=

Question

異質平等

我至今是：

module Foo 

postulate P : 'P 
postulate NP : 'NP 

complexityProof : P = NP 
complexityProof = ?complexityProof_rhs 

但在試圖加載該文件，我只是得到：

When elaborating type of Foo.complexityProof: 
When elaborating argument y to type constructor =: 
    Can't unify 
      'NP 
    with 
      'P 

    Specifically: 
      Can't unify 
        "NP" 
      with 
        "P" 

一個小的錯誤感到驚訝，因爲我伊德里斯認爲，具有異質性的「約翰梅傑」平等，在左右兩側有不同的類型。現在有一個不同的標誌？

Answer 1

從文檔：

注：伊德里斯平等類型是潛在的異質的，這意味着它是 可以潛在不同類型的值之間的狀態等式。 但是，伊德里斯會嘗試均勻的情況下，除非它不能檢查。

您可能需要使用（〜=〜）來顯式請求異構平等。

所以我不知道爲什麼=不工作，因爲我覺得文檔想說的是異構的平等是一個備用的，但你可以使用~=~代替：

module Foo 

postulate P : 'P 
postulate NP : 'NP 

complexityProof : P ~=~ NP 
complexityProof = ?complexityProof_rhs