如何在Lean中隐藏Prelude？类比Haskell的实现方式

在Haskell中，我们可以通过以下方式控制Prelude的导入：

• 完全隐藏Prelude：import Prelude ()
• 隐藏特定符号：import Prelude hiding (Bool)

但在Lean中直接照搬类似语法会报错，比如尝试open Init.Prelude ()会收到：

error: unexpected token ')'; expected identifier
尝试open Init.Prelude hiding Bool会收到：
error: unknown namespace 'Init.Prelude'

下面是正确的实现方式：

1. 完全禁用默认的Prelude（Init模块） #

Lean默认会自动导入Init模块（对应Haskell的Prelude）。如果要完全不加载这个默认模块，只需在文件最开头添加：

prelude

这会让Lean跳过所有默认的Init导入，和Haskell的import Prelude ()效果一致。

2. 隐藏特定符号 #

如果只想隐藏Init中的某个特定符号，有两种场景：

场景一：导入时隐藏符号 #

在导入Init模块时直接指定要隐藏的符号：

import Init hiding (Bool)

场景二：打开命名空间时隐藏符号 #

如果已经自动导入了Init，在打开其命名空间时可以通过hiding排除特定符号。注意Lean中没有Init.Prelude命名空间，直接使用Init或具体子命名空间即可：

-- 隐藏Init下的Bool符号
open Init hiding (Bool)

-- 更精确地隐藏Bool（因为Bool实际在Init.Data.Bool中）
open Init.Data.Bool hiding (Bool)

错误原因说明 #

• unknown namespace 'Init.Prelude'：Lean的默认基础模块是Init，不存在Init.Prelude这个命名空间，这是和Haskell的核心差异点。
• open ... ()：Lean的open语法不支持用()表示不打开任何符号，若无需打开命名空间，直接不写open语句即可；若要完全禁用默认导入，使用prelude指令。

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