我在两个不同的文件中有两个不同的模块签名。它们具有相同的字段名称,但行为不同。
而里面的函子定义了另一个函子。
PI.v
Module Type TPI.
Parameter sig : Signature.
Parameter trsInt: forall f, pi f.
End TPI.
Module P (Export T: TPI).
Lemma A...
Module Export Mono <: MonoType.
End P.
和
MI.v
Module Type TMI.
Parameter sig : Signature.
Parameter trsInt : forall f, mi f.
End TMI.
Module M (Export TM: TMI).
Lemma B ...
Module Export Mono <: MonoType.
End M.
例如,在MonoType
另一个文件中的位置Mono.v
这是我的情况。
我在该文件中调用了另一个文件B.v
,我需要在文件PI.v
和MI.v
.
例如,我需要同时使用它们的一个定义。
Definition redPair R is :=
match is with
| Type_PI => pi_int R is
| Type_MI => mi_int R is
end.
我有一个问题,R
因为pi_int R
并且mi_int R
有不同的sig
(签名),在模块签名内部使用并在pi_int
模块签名内部使用。trsInt
TPI
mint_int
trsInt
TMI
这是我定义它的方式:
Module PI (Import P : TPI).
Definition pi_int R is := P.trsInt ...
(* inside PI I define another functor for MI *)
Module MI (Import M : TMI).
Definition mi_int R is := M.trsInt ...
Definition redPair R is :=
match is with
| Type_PI => pi_int R is
| Type_MI => mi_int R is (* error here saying that it used the sig of
P.sig but in this case mi_int used the sig of M.sig *)
end.
End MI.
End PI.
我的问题是,有没有一种方法可以让我拥有一个良好的模块结构,我可以在定义处拥有相同的签名redPair
?感谢您的帮助。