编辑“︁Lean文档资源”︁（章节）

== Lean文档资源 ==

'''Lean文档资源'''是Lean编程语言及其相关生态系统的官方和社区维护的文档集合，为初学者和高级用户提供系统化的学习材料、API参考和实用指南。这些资源覆盖了从基础语法到高级定理证明的各个层面，是掌握Lean语言不可或缺的工具。

=== 核心文档类型 ===
Lean的文档体系包含以下主要类别：

{| class="wikitable"
! 文档类型 !! 内容描述 !! 适用阶段
|-
| '''官方教程''' || 交互式入门指南和语法基础 || 初学者
|-
| '''数学库文档''' || Mathlib库的API参考和模块说明 || 中高级
|-
| '''元编程手册''' || 宏系统和代码生成技术 || 高级
|-
| '''社区Wiki''' || 实战技巧和最佳实践 || 全阶段
|}

=== 官方教程示例 ===
以下展示官方教程中的基础代码示例，演示自然数加法：

<syntaxhighlight lang="lean">
-- 定义自然数加法函数
def add : Nat → Nat → Nat
  | n, zero   => n
  | n, succ m => succ (add n m)

-- 使用示例
#eval add 2 3  -- 输出: 5
</syntaxhighlight>

'''代码解析：'''
* 使用模式匹配定义递归加法
* <code>zero</code>和<code>succ</code>是自然数的构造子
* <code>#eval</code>命令执行运行时计算

=== 数学库文档结构 ===
Mathlib的文档采用分层架构：

<mermaid>
graph TD
    A[Mathlib] --> B[Algebra]
    A --> C[Analysis]
    A --> D[Topology]
    B --> B1[Group Theory]
    B --> B2[Ring Theory]
    C --> C1[Calculus]
    C --> C2[Measure Theory]
</mermaid>

关键搜索技巧：
* 使用<code>Ctrl+Space</code>触发自动补全
* 通过<code>#check</code>命令查看类型签名
* 使用<code>lake doc</code>生成本地文档

=== 文档查询实战 ===
当需要查找群论中的子群定义时：

<syntaxhighlight lang="lean">
import Mathlib.GroupTheory.Subgroup.Basic

#check Subgroup  -- 输出: Subgroup (G : Type u_1) [Group G] : Type u_1
</syntaxhighlight>

=== 公式渲染示例 ===
Lean支持在文档中嵌入数学公式，如群论公理：

<math>
\forall a,b,c \in G, (a \cdot b) \cdot c = a \cdot (b \cdot c)
</math>

=== 版本兼容性 ===
不同Lean版本的文档差异：

{| class="wikitable"
! 版本 !! 文档特性
|-
| Lean 3 || 经典数学库文档
|-
| Lean 4 || 改进的编译器文档
|}

=== 高级技巧 ===
1. 使用<code>@[doc]</code>属性添加自定义文档：
<syntaxhighlight lang="lean">
@[doc "计算斐波那契数列"]
def fib : Nat → Nat
  | 0 => 1
  | 1 => 1
  | n+2 => fib n + fib (n+1)
</syntaxhighlight>

2. 文档生成工具链：
* <code>lean --json</code>导出结构化文档
* <code>doc-gen4</code>生成HTML文档

=== 故障排查 ===
常见文档访问问题解决方案：
* 更新Lake包管理器：<code>lake update</code>
* 重建文档索引：<code>lake build +doc</code>
* 清除缓存：<code>rm -rf .lake/build/doc</code>

通过系统性地利用这些文档资源，开发者可以高效掌握Lean语言的各个知识层面，从基础编程到形式化验证。建议定期查阅最新官方文档以获取API变更信息。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean社区与资源]]