从实现模块中的模块签名导入注释

Question

如何使Category中定义的符号在HomCategory中可用？

Module Type Category.
  Parameter Object : Type.
  Parameter Arrow : Object -> Object -> Type.
  Infix "~>" := Arrow (at level 25) : category_scope.
  Open Scope category_scope.
  Delimit Scope category_scope with category.
  Bind Scope category_scope with Object Arrow.
  Variable id : forall a : Object, a ~> a.
  ...
End Category.
Module HomCategory <: Category.
  Definition Object := Type.
  Definition Arrow(a b : Object) := a -> b.
  Print Scope category_scope. (* Error: Scope category_scope is not declared. *)
  ...
End HomCategory.

Answer 1

恐怕真的没有办法做到这一点。Coq中模块的状态很奇怪，这意味着Module Type和该类型的东西之间的唯一连接是Coq检查定义是否与签名兼容。模块中的Arrow声明实际上并不是一个一流的实体。因此，不应该有一种方法来连接签名中定义的符号和实现。我想到了两种选择：

• 每当你想把你的符号用于新事物时，都要重新声明它们。

• 不要将模块用于特定多态性。对于规范结构或类型类，多态操作在理论上确实具有一流的地位，这使得定义此类泛型符号变得更容易。例如，请查看ssreflect中eqtype s的==表示法的定义：http://ssr.msr-inria.inria.fr/~jenkins/current/eqtype.html