我正在使用generalized rewriting features of Coq .
我想打印当前可用于setoid_rewrite的setoid和态射，以更好地理解重写失败时缺少哪个关系或函数。有什么办法可以做到吗？
最佳答案
也许打印实例...可以提供帮助。
Require Import Setoid.
Print Instances Equivalence.
Print Instances Morphisms.Proper.
来自您提供的手册页链接。
27.2.3 Printing relations and morphisms
The
Print Instancescommand can be used to show the list of currently registeredReflexive(usingPrint Instances Reflexive),SymmetricorTransitiverelations,Equivalences,PreOrders,PERs, and Morphisms (implemented asProperinstances). When the rewriting tactics refuse to replace a term in a context because the latter is not a composition of morphisms, thePrint Instancescommands can be useful to understand what additional morphisms should be registered.
关于coq - 在 Coq 中打印现有的 setoid 和态射，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/38281702/