Antoine Labelle (Jul 19 2022 at 16:22):
Why is there an empty file
category_theory/functor/default.lean? It only contains an import and nothing else.
Antoine Labelle (Jul 19 2022 at 16:23):
It seems to have been introduced in PR #12346.
Floris van Doorn (Jul 19 2022 at 16:25):
Probably to be backwards compatible, it allows you to write
import category_theory.functor to import
import category_theory.functor.default. That said, we can remove it.
Last updated: Aug 03 2023 at 10:10 UTC