我正在尝试在我的项目中使用模块，我做了这个小例子来展示我正在努力解决的问题。
Module Type A.
Parameter t : Type.
End A.
Module a : A.
Definition t := nat.
End a.
Module B.
Module Import InstanceOfA := a.
Definition x : t := 2.
Definition sum (t1 t2 : t) : nat := t1 + t2.
End B.
失败的原因是：
术语“2”的类型为“nat”，而预期的类型为“t”。
基本上，我有一个带有参数化类型的模块类型和一个实例化它的模块。该模块是自然数模块类型的特定实现（因此 t:=nat），因此当我尝试在第三方模块中使用该模块时，我想使用此实例来讨论自然数。
在我的真实场景中，我有一些想要开始工作的强制。我知道，如果我在模块 B 中使用 Nats，A 中的定义会正常工作，但会发生的情况是我获得了 type 的值t，并且需要将它们视为 type nat。
是否有机会从模块中“暴露”类型相等性？我尝试了类似身份函数的东西：t -> nat但a它不起作用。
有可能吗？
不是
Module a : A.密封模块（从而隐藏 的定义t），而是 writeModule a <: A.，它使a的定义保持可见。