这个问题已经困扰我太多次了。有没有办法在 Coq 中打印模块类型的每个元素的签名。
例如：
Print Orders.OrderedType.
Module Type Orders.OrderedType = Sig
Parameter t
Parameter eq
Parameter eq_equiv
Parameter lt
Parameter lt_strorder
Parameter lt_compat
Parameter compare
Parameter compare_spec
Parameter eq_dec
End
Print Module Type Orders.OrderedType.
Module Type Orders.OrderedType = Sig
Parameter t
Parameter eq
Parameter eq_equiv
Parameter lt
Parameter lt_strorder
Parameter lt_compat
Parameter compare
Parameter compare_spec
Parameter eq_dec
End
About Orders.OrderedType.
Module Type Coq.Structures.Orders.OrderedType
所有这些都是无用的，因为它们不会让我想起每个元素的类型......
而且我什至不能使用错误消息来提醒我，因为它们很愚蠢：
Error: Signature components for label eq do not match.
确定错误信息，不要告诉我预期的类型...
我不知道这是否已在 8.4 中修复，但我真的很想有一种方法不必寻找它的定义位置，以便提醒它是如何定义的。有这样的事吗？:(
特别是，找出定义只是沿着一个可笑的长链模块组合追逐......说真的：
Module Type OrderedType <: DecidableType := DecStrOrder <+ HasEqDec.
是的，谢谢...
Module Type DecStrOrder := StrOrder <+ HasCompare.
继续...
Module Type StrOrder := EqualityType <+ HasLt <+ IsStrOrder.
...
Module Type EqualityType := Eq <+ IsEq.
当然...
Module Type Eq := Typ <+ HasEq.
好的...
Module Type Typ.
Parameter Inline(10) t : Type.
End Typ.
最后，我知道了的类型t！\o/