importing multiple files at once

Stream: new members

[Connor Gordon]

If I wanted to import everything in, say, set_theory.ordinal into a Lean file, how would I go about doing that? I recognize that I can import every file individually but I'd imagine there is some way to do it with a single import.

[Kevin Buzzard]

If you really need that and if it doesn't exist already you can just create a new file set_theory.ordinal.default in mathlib which just contains lines importing every other file in the directory and then you can import it with import set_theory.ordinal. But imports are transitive so if you just import a couple of well-chosen ones all the rest will be included, and that's probably the easier option

[Connor Gordon]

Alright, that sounds reasonable. Thanks!