我目前正在与 vellvm 合作，对其进行改造。我是一个coq新手。
在编程时，我遇到了以下警告:
Warning: Stack overflow or segmentation fault happens when working with large numbers in nat (observed threshold may vary from 5000 to 70000 depending on your system limits and on the command executed).
我生成此警告的函数会计算签名。签名分为上位和下位。给定两个 n1 和 n2 表示高位和低位，它计算 (n1*65536)+n2 - 这是并排放置两个 16 位二进制数的抽象。
我很惊讶，因为 coq nat 定义似乎可以从外部处理大整数，这要归功于 S 构造函数。
我应该如何避免此警告/在 coq 中使用大数字？
我愿意将实现从 nat 更改为某种二进制结构。
谢谢!
最佳答案
而不是使用 nat输入 Coq，有时(当您必须操作大数字时)使用 Z 更好类型，它是使用符号幅度对表示的整数形式化。权衡是您的证明可能会稍微复杂一些； nat非常简单，因此承认简单的证明原则。
然而，在 Coq 中，广泛使用了符号来简化定义、定理和证明的编写。 Coq 有一个非常小的内核(我们想要这个是因为我们希望能够相信证明检查器是正确的，我们可以阅读它)，上面有很多符号。然而，由于事物有不同的表示，而且只有少数几个好的符号，我们的符号通常会发生冲突。为了解决这个问题，coq 使用 interpretation scopes消除符号的歧义，并将它们解析为名称(因为“+”表示 add 、 plus 等......)。
你是对的，使用 Z_scope在哪里，+为 plus内Z .
关于binary - 如何避免 Coq nats 中的堆栈溢出或段错误？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/13662274/