coq - 在 Coq 中打印现有的 setoid 和态射

Question

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

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

Answer 1

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

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

从您提供的手册页链接。

27.2.3 打印关系和态射

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