この問題は、私を何度も悩ませてきました。モジュール型の各要素の署名を 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.
Ok...
Module Type Typ.
Parameter Inline(10) t : Type.
End Typ.
最後に、私はt!の型を知っています。\o/