小编pdx*_*eif的帖子

到目前为止我所拥有的是：

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"

对这个错误有点惊讶，因为我认为伊德里斯具有异构的“约翰·梅杰”平等，可以很好地处理 = 左侧和右侧的不同类型。现在有不同的符号了吗？