Eric Wieser (Jan 06 2022 at 15:32):
I was a bit dismayed to see that after editing something low in the heirarchy, I have to wait for most of the topology library to compile before being able to build file#data.complex.basic (import graph). The culprit is file#data/real/sqrt (import graph), which pulls in large amounts of topology so that it can state that sqrt is continuous.
Does it seem reasonable to split out the continuity statements from data/real/sqrt? If so, what would be a better home for them?
Yury G. Kudryashov (Jan 06 2022 at 19:12):
Yury G. Kudryashov (Jan 06 2022 at 19:13):
--old you don't have to care too much about things like this.
Yury G. Kudryashov (Jan 06 2022 at 19:14):
(And I think that we should make
real depend on
Last updated: Aug 03 2023 at 10:10 UTC