Drucken Sie bestehende Seetoids und Morphismen in Coq

Question

Ich verwende die generalized rewriting features of Coq.

Ich möchte die derzeit verfügbaren setoid_rewrite Seetoids und Morphismen drucken, um besser zu verstehen, welche Relation oder Funktion fehlt, wenn das Umschreiben fehlschlägt. Gibt es eine Möglichkeit, das zu tun?

Answer 1

Vielleicht kann Print Instances ... helfen.

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

Von der Man-Seite Link zur Verfügung gestellt.

27.2.3 Druck Beziehungen und morphisms

Der Print Instances Befehl können die Liste der aktuell Reflexive registriert (mit Print Instances Reflexive), Symmetric oder Transitive Beziehungen, Equivalence s, PreOrder s zu zeigen, verwendet werden, PER s und Morphismen (implementiert als Proper Instanzen). Wenn die Umschreibtaktik ablehnt, um einen Begriff in einem Kontext zu ersetzen, weil letzterer keine Komposition von Morphismen ist, können die Print Instances Befehle nützlich sein, um zu verstehen, welche zusätzlichen Morphismen registriert werden sollten.