2

我正在使用Coq 的广义重写功能

我想打印当前可用的 setoid 和态射setoid_rewrite,以便更好地了解重写失败时缺少哪个关系或函数。有没有办法做到这一点?

4

1 回答 1

2

也许Print Instances ...可以提供帮助。

Require Import Setoid.
Print Instances Equivalence.
Print Instances Morphisms.Proper.

从您提供的手册页链接。

27.2.3 打印关系和态射

Print Instances命令可用于显示当前注册的列表Reflexive(使用Print Instances ReflexiveSymmetricTransitive关系、Equivalences、PreOrders、PERs 和 Morphisms(作为Proper实例实现)。当重写策略拒绝替换上下文中的术语时,因为后者不是态射的组合,这些Print Instances命令有助于理解应该注册哪些额外的态射。

于 2016-07-11T07:43:24.280 回答