Stream: Coq users

Topic: sharing module parameters

view this post on Zulip Philipp G. Haselwarter (Dec 07 2020 at 17:29):

I used to have a large file, which contained a module M parametrised by a module A. I want to split the file containing M into several files, say f1, f2, f3, containing M1, M2, M3 respectively. Each of these will have to rely on the preceding ones. I could parametrise all of them by A, but how do I ensure that once I'm done, I can bundle it up in such a way that each of M1, M2, M3 make coherent assumptions? I.e. I don't want to deal with M1(A) being different from what M2(A) thinks M1(A) should be?

view this post on Zulip Matthieu Sozeau (Dec 07 2020 at 21:42):

I think with Functors and Include M1(A) in M2 you should be fine

Last updated: Jun 23 2024 at 23:01 UTC