79500510

Date: 2025-03-11 11:09:20
Score: 2.5
Natty:
Report link

I cannot reproduce on Mathlib (which was the Lean project I happened to have open when I read your question)

buzzard@brutus:~/mathlib/Mathlib$ cat > A.lean
namespace inner
buzzard@brutus:~/mathlib/Mathlib$ cat > B.lean
namespace inner
buzzard@brutus:~/mathlib/Mathlib$ cat > C.lean
import Mathlib.A
import Mathlib.B

I can open C.lean without any errors. Indeed this pattern is commonplace in mathlib. Are you sure you've diagnosed your problem correctly?

Reasons:
  • Blacklisted phrase (0.5): I cannot
  • Has code block (-0.5):
  • Ends in question mark (2):
  • Low reputation (0.5):
Posted by: Kevin Buzzard