coq - 为什么 Coq 中的所有数字文字都显示 nat 类型？

Question

我试图在 Coq 中使用更大的数字，其中内置的 Nat 类型不合适。所以我试图用正类型或 N 类型建立特定的值。

根据 BinNums 的标准库文档：

正数也将使用十进制表示法表示；例如 6%positive 将缩写为 xO (xI xH)

N 中的数字也将使用十进制表示法表示；例如 6%N 将缩写为 Npos (xO (xI xH))

但是我的 Coq 代码仍然给我 Nat 输入的数字：

From Coq
Require Import BinNums.

Definition sixp := 6%positive.
Definition sixn := 6%N.

Check sixp.
Check sixn.

结果：

sixp
     : nat

sixn
     : nat

我哪里错了？

标签： coq

Answer 1

From Coq Require Import NArith.

应该解决这个问题。

这里的问题是BinNums不导出任何定义相应数字符号的模块，请参阅此处了解更多详细信息。

您需要的数字符号位于BinPosDef和BinNatDef模块中并NArith重新导出它们。