导入QArith后定义产品类型

费德里科

导入QArithCoq后

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".

如何使用原件*

安东·特鲁诺夫(Anton Trunov)

从某种意义上说,没有“原始的” *符号可以重载和重用,通常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] 删除。

编辑于
0

我来说两句

0 条评论
登录 后参与评论

相关文章

根据产品类型定义递归函数

从自定义产品类型创建产品

Woocommerce产品类型简码

每个产品类型的 PDP

根据产品类型向产品价格添加自定义文本标签

在WooCommerce 4中以编程方式从自定义产品类型添加新产品

如何仅为自定义产品类型定义字段-Woo Commerce Hook

如何配置构建类型与产品类型?

按产品类型配置applicationId后找不到R类

WooCommerce自定义产品类型-多个添加到购物车部分的问题

如何在WooCommerce中为自定义产品类型启用价格和库存

在WooCommerce自定义产品类型上显示库存状态

如何检查WooCommerce中的自定义产品类型选项?

定义具有最少固定点,总和和产品类型的列表

如何在 Woocommerce 的自定义产品类型中添加变体选项卡?

使用ACF编号字段作为WooCommerce自定义产品类型的价格

在WooCommerce中更改自定义产品类型的订单运送地址

产品类型的相互递归函数

在Woocommerce上处理产品类型

转到如何检查产品类型

GetProductInfo-pdwReturnedProductType含义(产品类型)?

linq-to-sql产品类型的IQueryable <???>

Elasticsearch部分产品类型名称

解析产品类型的CLI选项

Magento-删除产品类型选项

在 WooCommerce 循环产品标题后显示来自产品类别的自定义字段

在WooCommerce中将自定义标签添加到特定产品类型的单个产品页面

如何从产品实体(Drupal贸易)获取产品类型?

按产品类型查询/过滤woocommerce产品