Topic: circular imports in mathlib
Kevin Buzzard (Oct 02 2018 at 13:58):
Johannes said in the p-adic PR
I'm fine with merging, with one exception: Please don't import topology in
data/polynomial. I guess we need a
analysis/polynomial.leanfor the continuity statement.
I don't like this, as we get into a huge mess if we have too much cyclic dependencies between the top level directories. I think
datashouldn't depend on
I've never thought about these issues. Are there general rules written down somewhere about what is acceptable and what is not when it comes to this sort of question?
Last updated: May 18 2021 at 07:19 UTC