使用异质等式 =

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

从文档中：

注意：Idris 的相等类型可能是异构的，这意味着可以在潜在不同类型的值之间声明相等。然而，Idris 将尝试同类情况，除非它无法进行类型检查。

您可能需要使用 (~=~) 来显式请求异构平等。

所以我不确定为什么=不起作用，因为我认为文档试图说异构平等是一种后备，但你可以使用~=~：

module Foo

postulate P : 'P
postulate NP : 'NP

complexityProof : P ~=~ NP
complexityProof = ?complexityProof_rhs