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

Question

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

根据BinNums:的标准库文档

正数也将使用十进制表示法表示；例如6%的阳性将缩写为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

我哪里错了？

Answer 1

From Coq Require Import NArith.

应该解决这个问题。

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

您需要的数字符号位于BinPosDef和BinNatDef模块中，NArith会重新导出这些符号。

Answer 2

我找到了一种解决这个问题的方法。使用AltBinNotations模块。

我不知道是否有更好的方法。

注意：在Coq8.8之前，正、N、Z类型的文字是使用名为bigint.ML的任意精度整数的本地ML库解析和打印的。从8.9开始，默认情况下是使用转换数字序列的Coq库进行解析和打印，从而减少了需要信任的ML代码量。但是这种方法比较慢。然后，这个文件提供了对遗留方法的访问权限，在依赖bigint.ML的更大ML信任基础上进行效率交易

From Coq
Require Import BinNums.
From Coq
Require Import AltBinNotations.
Definition sixp : positive := (6%positive).

sixp已定义。

sixp：阳性