1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
|
Module Type TA.
Parameter t : Set.
End TA.
Module Type TB.
Declare Module A: TA.
End TB.
Module Type TC.
Declare Module B : TB.
End TC.
Module Type TD.
Declare Module B: TB .
Declare Module C: TC
with Module B := B .
End TD.
Module Type TE.
Declare Module D : TD.
End TE.
Module Type TF.
Declare Module E: TE.
End TF.
Module G (D: TD).
Module B' := D.C.B.
End G.
Module H (F: TF).
Module I := G(F.E.D).
End H.
Declare Module F: TF.
Module K := H(F).
|