Geek Answers Handbook

Import record from the module signature in the implementation module

How to make the notation defined in Categoryavailable in 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.
+4
source share
1 answer

I am afraid that this is actually not the case. The status of the modules in Coq is weird, which means that the only connection between Module Typeand something with this type is that Coq checks that the definitions are compatible with the signature. An ad Arrowinside a module is not a first-class asset. Therefore, there should be no way to establish a connection between the designation defined in your signature and your implementation. There are two alternatives that come to my mind:

+2

More articles:


All Articles