编辑“︁Lean4新标准库”︁（章节）

== 主要特性 ==  
=== 1. 模块化设计 ===  
Lean4标准库采用分层模块结构，允许用户按需导入功能，减少编译开销。核心模块包括：  
* '''Init''': 基础类型（如`Nat`, `List`, `Option`）和最小依赖的核心函数。  
* '''Mathlib'''（兼容层）: 提供与Lean3 Mathlib兼容的接口。  
* '''System''': 文件IO、进程管理等系统操作。  

示例：导入`List`模块  
<syntaxhighlight lang="lean">  
import Std.Data.List.Basic  
-- 现在可使用List相关函数  
</syntaxhighlight>  

=== 2. 改进的数据类型 ===  
新库优化了常用数据类型的实现，例如：  
* '''List''': 新增高效切片操作和惰性求值支持。  
* '''Array''': 基于可变数组的实现，性能更优。  
* '''HashMap''': 使用哈希冲突优化算法。  

示例：使用`Array`  
<syntaxhighlight lang="lean">  
def arr : Array Nat := #[1, 2, 3]  
#eval arr.push 4  -- 输出: #[1, 2, 3, 4]  
</syntaxhighlight>  

=== 3. 定理证明工具增强 ===  
标准库内置更多自动化策略和简化器，例如：  
* '''simp''': 支持自定义化简规则集。  
* '''omega''': 线性算术决策过程。  

示例：证明列表长度守恒  
<syntaxhighlight lang="lean">  
theorem list_length_cons (x : Nat) (xs : List Nat) :  
  (x :: xs).length = xs.length + 1 := by simp  
</syntaxhighlight>