idris - 使用带 = 的异质相等

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"

对这个错误有点惊讶，因为我认为 Idris 具有异构的“John Major”相等性，在 = 的左侧和右侧使用不同的类型很好。现在有一个不同的符号？

Answer 1

从文档中：

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

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

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

module Foo

postulate P : 'P
postulate NP : 'NP

complexityProof : P ~=~ NP
complexityProof = ?complexityProof_rhs