在 Coq 中打印现有的 setoids 和态射
Print existing setoids and morphisms in Coq
我正在使用 generalized rewriting features of Coq。
我想打印 setoid_rewrite 当前可用的 setoids 和态射，以便更好地理解重写失败时缺少哪个关系或函数。有什么办法吗？
也许 Print Instances ... 可以提供帮助。
Require Import Setoid.
Print Instances Equivalence.
Print Instances Morphisms.Proper.
来自您提供的手册页 link。
27.2.3 Printing relations and morphisms
The Print Instances command can be used to show the list of currently
registered Reflexive (using Print Instances Reflexive), Symmetric or
Transitive relations, Equivalences, PreOrders, PERs, and Morphisms
(implemented as Proper instances). When the rewriting tactics refuse
to replace a term in a context because the latter is not a composition
of morphisms, the Print Instances commands can be useful to understand
what additional morphisms should be registered.
我正在使用 generalized rewriting features of Coq。
我想打印 setoid_rewrite 当前可用的 setoids 和态射，以便更好地理解重写失败时缺少哪个关系或函数。有什么办法吗？
也许 Print Instances ... 可以提供帮助。
Require Import Setoid.
Print Instances Equivalence.
Print Instances Morphisms.Proper.
来自您提供的手册页 link。
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.