编辑“︁Lean不可变数据结构”︁（章节）

== 基本原理 ==
在Lean中，当对数据结构进行操作时（如向列表添加元素），系统会创建新结构而非修改原结构。例如：

<syntaxhighlight lang="lean">
-- 定义一个列表
def originalList := [1, 2, 3]

-- "添加"元素（实际创建新列表）
def newList := 0 :: originalList

-- 输出结果
#eval originalList  -- [1, 2, 3]
#eval newList       -- [0, 1, 2, 3]
</syntaxhighlight>

注意：<code>originalList</code>未被修改，<code>::</code>操作符创建了包含新元素的新列表。

=== 内存效率 ===
Lean通过'''结构共享'''优化内存使用。新旧版本共享未修改的部分：

<mermaid>
graph LR
    A[newList] --> B[0]
    A --> C[originalList]
    C --> D[1]
    D --> E[2]
    E --> F[3]
</mermaid>

数学上，这种操作的时间复杂度为<math>O(1)</math>，因为只需分配一个新节点并指向原有结构。