Zulip Chat Archive

Stream: new members

Topic: importing multiple files at once


Connor Gordon (Oct 25 2022 at 03:08):

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 (Oct 25 2022 at 05:23):

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 (Oct 26 2022 at 00:24):

Alright, that sounds reasonable. Thanks!


Last updated: Dec 20 2023 at 11:08 UTC