I am using the generalized rewriting features of Coq.
I would like to print the setoids and morphisms currently available to setoid_rewrite
, to understand better which relation or function is missing when rewriting fails. Is there any way to do that?
Perhaps Print Instances ...
can help.
Require Import Setoid.
Print Instances Equivalence.
Print Instances Morphisms.Proper.
From the man page link you provided.
27.2.3 Printing relations and morphisms
The
Print Instances
command can be used to show the list of currently registeredReflexive
(usingPrint Instances Reflexive
),Symmetric
orTransitive
relations,Equivalence
s,PreOrder
s,PER
s, and Morphisms (implemented asProper
instances). When the rewriting tactics refuse to replace a term in a context because the latter is not a composition of morphisms, thePrint Instances
commands can be useful to understand what additional morphisms should be registered.