导入QArith
Coq后
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".
如何使用原件*
?
从某种意义上说,没有“原始的” *
。符号可以重载和重用,通常Coq足够聪明,可以为符号选择正确的解释。但是有时您需要明确地告诉Coq使用什么解释范围。
参考手册指出(第12.2节):
解释范围是术语解释的一组符号。解释作用域提供了一种薄弱的,纯粹的语法形式的符号重载:相同的符号(例如infix符号
+
)可用于表示加法运算符的不同定义。根据当前打开的解释范围,解释会有所不同。解释范围可以包括对数字和字符串的解释。
让我提到一个有用的命令,以了解有关符号及其解释范围的更多信息:Locate "*".
将为您提供*
展开的内容列表,以及解释范围的名称和默认解释范围。
从版本8.4pl4开始的Coq尝试使用默认的解释范围,Q_scope
在您的情况下,这就是您看到错误的原因。它可以很容易地修复,例如使用范围注释:
Definition TT : Type := (T * T) % type.
但是,较新的Coq版本(如8.7.0)理解在这种情况下,我们应该使用type_scope
,因此您的代码段无需进行任何修改即可工作。
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句