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
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
Btw, when you say 'module' do you mean a '.lean file'? ie. is there a 1:1 mapping between them?
1
Oh yes, that is correct. I should have clarified that. Between existing support for namespaces and typeclasses and the unlikeliness of adding modules to the kernel, I don't see any place for finer-grained modules in Lean.
2
Show replies