在 Idris 中证明函数的计算结果为 True

Question

编辑：我发现如果我直接内联 t1 的定义，那么这种类型检查就很好。因此，该定义似乎只是将 t1 视为一个未知变量，而不是我之前的实际定义。有什么办法可以强制执行此操作吗？

前言：我完全意识到这不是写这篇文章的惯用方式。我只是想具体了解这里发生了什么。

我已经编写了一个二叉树的简单实现和一个函数 elemBT，它检查树是否包含特定元素并评估为布尔值（想想 Haskell 的 elem 函数，二叉树除外）。

t1 : BT Nat
t1 = Node 5 Nil Nil

elemBT : Eq a => a -> BT a -> Bool

> elemBT 5 t1
True : Bool

现在我知道 elemBT 的计算结果为 True，我希望能够编写一个非常简单的语句，通过执行以下操作来证明这一点。

t1contains5 : elemBT 5 t1 = True
t1contains5 = Refl

有点出乎意料的是，这导致了统一失败。但是，我可以使用内置列表做几乎完全相同的事情。

junk : elem 5 [1,5] = True
junk = Refl

而且这种类型的检查符合预期。为什么我的二叉树示例的工作方式不同？

谢谢。

Answer 1

我自己解决了这个问题。事实证明，最近某个时候（可能是 2015 年底）对 Idris 进行了更改，将任何小写字母、潜在隐式变量视为隐式变量。如果我将 T1 大写，那么这个问题就完全消失了。

中有一些进一步的讨论

Proving function evaluates to True in Idris