我如何写关于私有实现的证明?

Question

我想写一个关于我的函数的证明

export
foo : Nat -> Nat

但是因为只有export而不是public export，我怎么做呢?Afaikpublic使实现公开。

Answer 1

有时可以导出一个证明，证明该函数在扩展上等于您公开导出的函数。这样你就不会泄露你不想泄露的实现细节了。

Answer 2

非public export定义的实际实现可能仍然需要在同一模块中的定义(例如展开引理或证明定义在外延上等于Ohad建议的其规范)进行类型检查。

为此，Idris检查当前证明是否在引入私有定义的命名空间的子命名空间中，以决定是否对其进行约简。

因此，你可以证明子命名空间中不透明定义的属性，例如，如果reverse被定义在Data.List中，你可以定义一个模块Data.List.Properties，即使它仅仅是exported，它也会减少。

这目前也可以跨包工作。但使用风险自负:这在道德上是一种hack和

1. 如果上游包决定更改非公共定义(他们可能认为这不会破坏向后兼容性)，您的证明将会失效

2. 该语言的未来版本可能会考虑收紧此检查，以避免能够跨包使用此hack。

Answer 3

要么将证明写在与foo相同的文件中，要么将foo设为public export