Philipp G. Haselwarter (Dec 07 2020 at 17:29): 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?
Matthieu Sozeau (Dec 07 2020 at 21:42):I think with Functors and Include M1(A) in M2 you should be fine
Last updated: Apr 16 2024 at 17:01 UTC