Zulip Chat Archive

Stream: general

Topic: category_theory/functor/default

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: Dec 20 2023 at 11:08 UTC