feat: add module system appendix #514
Conversation
| Note also that `import all` is more powerful than the basic `import` before the module system as it allows for accessing imported private definitions directly by name, as if they were defined in the current module. | ||
| Thus another use case of `import all` is to make declarations available that need to be used in multiple modules but should not leak outside the current library. | ||
|
|
||
| `public import all M` behaves like `public import M` followed by `import all M`, i.e. the `all` modifier becomes irrelevant for downstream modules. |
There was a problem hiding this comment.
I wonder if this is really helpful (because it looks like the all is made public), or if we should require writing
public import M
import all M
instead, unless this is a common idiom.
There was a problem hiding this comment.
Even if it's common, I have the same gut feeling when seeing presentations and reading the text. It feels like a footgun.
There was a problem hiding this comment.
I had exactly the same thought after writing the paragraph, let's do it!
| [^meta3]: Semantically unrelated to the modifier of the same name in Lean 3. | ||
|
|
||
| A `meta` definition may access (and thus invoke) any `meta` or non-`meta` definition of the current module. | ||
| For accessing imported definitions, the definition must either have been marked as `meta` when it was declared or the import must be marked as such (`meta import` when the accessing definition is in the private scope and `public meta import` otherwise). |
There was a problem hiding this comment.
A question I have when reading this is whether meta import is a superset of import or whether it's orthogonal.
There was a problem hiding this comment.
I'm not completely sure yet to be honest; it is currently implemented as a superset. But a public meta import would not necessarily have imply public import if the imported declarations are used only in the bodies of public declarations.
There was a problem hiding this comment.
I would think that my imports for purposes of metaprogramming/code generation should be reasonably distinct from my imports for purposes of generated run-time code, so that I could depend on a heavyweight library for proof automation but distribute an executable that's independent of it.
There was a problem hiding this comment.
Ah you are right of course, we need to change that for the executable size goal
|
It looks like a GH Action we depended on got deleted. Rebase on |
Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
|
Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit 02ea616. |
3 participants
No description provided.