如何解决Lean4命名空间冲突？是否支持类似Haskell的限定导入？

当导入的多个模块存在同名命名空间（如示例中A、B文件的inner命名空间）导致冲突时，Lean4提供了多种无需修改原文件的解决方式，核心是通过别名导入区分不同来源的代码：

1. 给整个模块设置别名 #

通过import ... as语法给导入的模块分配别名，后续通过别名+命名空间的方式访问目标定义：

import Lab.A as A
import Lab.B as B

-- 访问A文件中的inner.f
#check A.inner.f -- 输出: A.inner.f : Nat
-- 访问B文件中的inner.f
#check B.inner.f -- 输出: B.inner.f : Nat

2. 仅导入目标命名空间并设置别名 #

如果不需要导入整个模块，可精准导入指定命名空间并设置别名，减少全局命名污染：

import Lab.A (inner as A_inner)
import Lab.B (inner as B_inner)

#check A_inner.f -- 输出: A_inner.f : Nat
#check B_inner.f -- 输出: B_inner.f : Nat

3. 局部打开命名空间简化书写 #

如果某段代码只需要使用其中一个命名空间的内容，可通过open ... in局部打开，避免重复写别名：

import Lab.A as A
import Lab.B as B

-- 局部打开A的inner命名空间，直接用f指代A.inner.f
def calcA :=
  open A.inner in
  f + 5

-- 局部打开B的inner命名空间，直接用f指代B.inner.f
def calcB :=
  open B.inner in
  f * 3

以上方法均无需修改原文件（包括外部库文件），完全适配你的场景。

内容的提问来源于stack exchange，提问作者Ireina