问题标签 [totality]

我正在使用抽象语法树，我想给活页夹自己的类型。这似乎给 Idris 的整体检查带来了问题……

使用典型的自我参照TreeIdris 可以很好地进行整体检查。

同样与相互Tree：

但是，通过参数化提取的类型来引入间接性，并且整体检查失败：

有没有办法让 Idris 正确检查最后一种递归类型的整体性？除此之外，除了在代码上撒上assert_totals 之外，还有什么其他的吗？

我编写了以下类型来编码其中所有可能的有理数：

请注意，PosN Z实际上编码 number 1，而NegN Z编码-1. 我更喜欢这样的对称定义，而不是Data.ZZmodule 给出的定义。现在我很难说服 Idris 将这些数字相加是总数：

有趣的是，当我在 Atom 编辑器中按 Alt-Ctrl-R 时一切正常（即使使用%default total指令）。但是，当我将其加载到 REPL 中时，它会警告我这plus可能不是全部：

从消息中我了解到它担心这些递归调用plus模式处理比率。我认为断言a小于Ratio a betc. 可以解决问题，但它没有，所以 Idris 可能看到了这一点，但遇到了其他问题。不过，我无法弄清楚它可能是什么。

我试图将每个整数形式化为自然数对的等价类，其中第一个分量是正数部分，第二个分量是负数部分。

Definition integer : Type := prod nat nat.

我想定义一个规范化函数，其中正负尽可能取消。

然而 Coq 说：

错误：规范化的递归定义格式不正确。在环境 normalize : integer -> integer i : integer a : nat b : nat a' : nat b' : nat 对 normalize 的递归调用的主要参数等于“(a', b')”而不是“i”的子项”。

我认为这可能与有根据的递归有关？

考虑以下（非常简化的）示例，该示例通过对其值的附带条件来约束数据类型：

有什么办法可以省略或总结这些impossible案例，而 Idris 仍然认为该功能是完整的吗？如果我确实留下了一个案例，我会得到类似的东西

我也不能只是一个包罗万象的情况，因为编译器不知道_不能是 Car 所以第二行不进行类型检查：

这给

我已经浏览了这篇文章中关于约束数据类型的想法，但我没有看到任何有用的方法。

在实际代码中这是简化而来的，有很多情况需要单独排出，非常笨拙。

这里我的意思是公理，我们可以Axiom在 Coq Gallina 中使用关键字来定义，而不是通过传递给 Coq 的命令行参数。

我知道一些公理使 Coq 不一致。然而，AFAIK 他们并没有使 Coq Turing 完整。在我粗略的理解中，这是因为它们不提供任何额外的计算行为。

有没有一个让 Coq 变得完整？如果不是，您能否更具体地解释为什么这是不可能的？

此 Idris 函数无法成功检查整体性，但在我看来，似乎涵盖了所有情况。这是我在合并排序中的合并功能。

使用 Idris 1.3.3 版

错误。

伊德里斯。

我正在使用 C 并且我调用的函数返回一个int表示 gt、eq 或 lt 的函数。我想在任何不应该发生的 1、0 或 -1 cos 上崩溃。我希望 Idris 将 0、1 和 -1 视为详尽匹配。我试过

但我明白了