Half-cooked thoughts about a proper module system for Lean 4
Conversation
Replying to
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:
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 😅
Replying to
We have something like that, I think it's mentioned in their related work :) . No direct relation with phases though (afaik), this is about ordering expansion steps within a phase.
1
1
Ah sorry! Yeah, still getting my head around all of this stuff!
1
Show replies