Stream: Coq users

Topic: Composition of Module Functors

view this post on Zulip Josh Cohen (Feb 27 2024 at 23:17):

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).

view this post on Zulip Michael Soegtrop (Feb 28 2024 at 08:47):

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.

view this post on Zulip Josh Cohen (Feb 28 2024 at 17:08):

Thank you!

Last updated: Jun 22 2024 at 16:02 UTC