我目前正在使用vellvm，对其进行转换。我是一个coq新手。
在编程时，我遇到了以下警告：
警告：在 nat 中处理大量数字时会发生堆栈溢出或分段错误（观察到的阈值可能在 5000 到 70000 之间变化，具体取决于您的系统限制和执行的命令）。
我生成此警告的函数会计算签名。签名分为上位和下位。给定两个代表高位和低位的 nat n1 和 n2，它计算 (n1*65536)+n2 - 这是并排放置两个 16 位二进制数的抽象。
我很惊讶，因为 coq nat 定义似乎可以处理来自外部的大整数，这要归功于 S 构造函数。
我应该如何避免这个警告/在 coq 中使用大数字？我愿意将实现从 nat 更改为某种二进制结构。
谢谢！
除了nat在 Coq 中使用类型，有时（当您必须处理大数字时）使用Z类型更好，这是使用符号大小对表示的整数形式化。权衡是您的证明可能会变得稍微复杂一些。nat非常简单，因此承认简单的证明原则。
然而，在 Coq 中，符号的广泛使用使编写定义、定理和证明变得更简单。Coq 有一个非常小的内核（我们想要这个是因为我们希望能够相信证明检查器是正确的，并且我们可以阅读它）上面有很多符号。然而，由于事物的表示方式不同，而且只有少数好的符号，我们的符号通常会发生冲突。为了解决这个问题，coq 使用解释范围来消除符号的歧义，并将它们解析为名称（因为“+”表示add,plus等...）。
你是对的，使用Z_scope是 where，+for pluswithin Z。