In lean4 I cannot rename imported files, which makes me confused on how to resolve name conflicts.

Suppose I have two files named A and B, each has a namespace inner and a f,

—- A
namespace inner
def f := 1

—- B
namespace inner
def f := 2

then in file C, if I import A and B, the compiler report error that name inner environment already contains inner.f.

import Lab.A
import Lab.B —- error environment already contains inner.f

Some files may be included from external libs so I cannot rely on renaming original file by hand.

How could I fix namespace problems like this? Also in lean4, do we have any thing like Haskell’s qualified import?

In lean4 I cannot rename imported files, which makes me confused on how to resolve name conflicts.

Suppose I have two files named A and B, each has a namespace inner and a f,

—- A
namespace inner
def f := 1

—- B
namespace inner
def f := 2

then in file C, if I import A and B, the compiler report error that name inner environment already contains inner.f.

import Lab.A
import Lab.B —- error environment already contains inner.f

Some files may be included from external libs so I cannot rely on renaming original file by hand.

How could I fix namespace problems like this? Also in lean4, do we have any thing like Haskell’s qualified import?

• compiler-errors
• lean

1 Answer 1

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?