Hello, how can I compose two module functors, as in the following example? Thanks
Module Type A.
End A.
Module Type B.
End B.
Module Type C (Y: B).
End C.
Module MakeB (X: A) : B.
End MakeB.
Module MakeC (Y: B) : C(Y).
End MakeC.
(*Doesn't work*)
Module MakeBC (X: A) := MakeC (MakeB X).
The problem with such constructions would be that the intermediate modules would not have a name. For this reason one has to explicitly name the modules and then include them as in:
Module MakeBC (X: A).
Module MyB := MakeB X.
Module MyC := MakeC MyB.
Include MyC.
End MakeBC.
The ref man says that an inline instantiation is just syntactic sugar for an include.
Thank you!
Last updated: Oct 13 2024 at 01:02 UTC