Coq模块Foo2中Search "foo"无结果？如何让foo可被搜索？

为什么Foo2内Search "foo"无结果？ #

当在Foo2中执行Include (Foo mt)时，虽然foo可以在当前模块中直接引用，但Coq的Search命令默认不会索引通过这种方式导入的参数化模块实例中的定义。这是因为Include参数化模块实例的行为是将实例内容"内联"到当前模块，但这些导入的定义并未被加入Search默认搜索的全局索引，也没有被标记为可被名称搜索到的顶层定义。

让foo对Search可见的方法 #

方法1：显式实例化并导入模块 #

将参数化模块Foo实例化后绑定到一个本地模块名，再导入该模块，这样Search就能索引到其中的定义：

Module Foo2 (mt : MT).
  Module F := Foo mt.
  Import F.

  (* 此时会输出：foo: 1 + 1 = 2 *)
  Search "foo".
End Foo2.

方法2：在Foo模块中添加导出声明 #

修改Foo模块，添加Export Foo.声明，让模块内容在被Include时自动被标记为可搜索：

Module Foo (mt : MT).
  Export Foo.

  (* prints: mt.f_thm: forall x : nat, mt.f x x *)
  Search "f_thm".

  Lemma foo : 1 + 1 = 2. Proof. reflexivity. Qed.

  (* prints: foo: 1 + 1 = 2 *)
  Search "foo".
End Foo.

Module Foo2 (mt : MT).
  Include (Foo mt).

  (* 此时会输出：foo: 1 + 1 = 2 *)
  Search "foo".
End Foo2.

内容的提问来源于stack exchange，提问作者andreas