使用带有=

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