我正在使用Coq 的广义重写功能。
我想打印当前可用的 setoid 和态射setoid_rewrite
,以便更好地了解重写失败时缺少哪个关系或函数。有没有办法做到这一点?
我正在使用Coq 的广义重写功能。
我想打印当前可用的 setoid 和态射setoid_rewrite
,以便更好地了解重写失败时缺少哪个关系或函数。有没有办法做到这一点?
也许Print Instances ...
可以提供帮助。
Require Import Setoid.
Print Instances Equivalence.
Print Instances Morphisms.Proper.
从您提供的手册页链接。
27.2.3 打印关系和态射
该
Print Instances
命令可用于显示当前注册的列表Reflexive
(使用Print Instances Reflexive
)Symmetric
或Transitive
关系、Equivalence
s、PreOrder
s、PER
s 和 Morphisms(作为Proper
实例实现)。当重写策略拒绝替换上下文中的术语时,因为后者不是态射的组合,这些Print Instances
命令有助于理解应该注册哪些额外的态射。