导入 QArith 后定义产品类型
Define product type after importing QArith
在 Coq 中导入 QArith 后
Require Import Coq.QArith.QArith_base.
我要定义一个产品类型
Parameter T : Type.
Definition TT : Type := T * T.
但是 * 在 QArith 中被重新定义，我收到错误消息
Error: The term "T" has type "Type" while it is expected to have type "Q".
如何使用原版*？
在某种意义上没有"original"*。符号可以重载和重用，通常 Coq 足够聪明，可以为符号选择正确的解释。但有时您需要明确告诉 Coq 使用什么解释范围。
参考手册说 (sect. 12.2):
An interpretation scope is a set of notations for terms with their interpretation. Interpretation scopes provide a weak, purely syntactical form of notation overloading: the same notation, for instance the infix symbol +, can be used to denote distinct definitions of the additive operator. Depending on which interpretation scope is currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings.
让我提一个有用的命令来找到更多关于符号及其解释范围的信息：Locate "*". 将为您提供 * 展开的事物列表，以及解释范围的名称和默认解释范围。
Coq 从版本 8.4pl4 开始尝试使用默认解释范围，在您的情况下为 Q_scope——这就是您看到错误的原因。它可以很容易地固定，例如带范围注释：
Definition TT : Type := (T * T) % type.
但是，较新的 Coq 版本（如 8.7.0）理解在这种情况下我们应该使用 type_scope，因此您的代码片段无需任何修改即可工作。
在 Coq 中导入 QArith 后
Require Import Coq.QArith.QArith_base.
我要定义一个产品类型
Parameter T : Type.
Definition TT : Type := T * T.
但是 * 在 QArith 中被重新定义，我收到错误消息
Error: The term "T" has type "Type" while it is expected to have type "Q".
如何使用原版*？
在某种意义上没有"original"*。符号可以重载和重用，通常 Coq 足够聪明，可以为符号选择正确的解释。但有时您需要明确告诉 Coq 使用什么解释范围。
参考手册说 (sect. 12.2):
An interpretation scope is a set of notations for terms with their interpretation. Interpretation scopes provide a weak, purely syntactical form of notation overloading: the same notation, for instance the infix symbol
+, can be used to denote distinct definitions of the additive operator. Depending on which interpretation scope is currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings.
让我提一个有用的命令来找到更多关于符号及其解释范围的信息：Locate "*". 将为您提供 * 展开的事物列表，以及解释范围的名称和默认解释范围。
Coq 从版本 8.4pl4 开始尝试使用默认解释范围，在您的情况下为 Q_scope——这就是您看到错误的原因。它可以很容易地固定，例如带范围注释：
Definition TT : Type := (T * T) % type.
但是，较新的 Coq 版本（如 8.7.0）理解在这种情况下我们应该使用 type_scope，因此您的代码片段无需任何修改即可工作。