Half-cooked thoughts about a proper module system for Lean 4
Conversation
Seeing as you were talking about metaprograms and Racket's phases, perhaps Klister's approach to 'stuck macros' would be interesting to look at, if you haven't seen it already. Not sure if it handles cross-module stuff though:
2
1
But perhaps it might be a bit more fancy than what you are after, or might not address your specific issues. Tbh it's still on my todo list to understand 😅