编辑“︁Lean注释”︁

{{DISPLAYTITLE:Lean注释}}

== 简介 ==
'''Lean注释'''是Lean编程语言中用于解释代码、添加文档说明或临时禁用代码段的重要工具。注释不会被编译器执行，但对代码可读性和维护性至关重要。Lean支持两种主要注释形式：单行注释和多行注释，同时也支持特殊的文档注释（Doc Strings）。

== 注释类型 ==

=== 单行注释 ===
单行注释以<code>--</code>开头，直到行尾结束：
<syntaxhighlight lang="lean">
-- 这是一个单行注释
def hello := "world"  -- 这里可以添加行内注释
</syntaxhighlight>

=== 多行注释 ===
多行注释使用<code>/-</code>开始，<code>-/</code>结束：
<syntaxhighlight lang="lean">
/-
这是一个跨越多行的
注释块
-/
def add (x y : Nat) := x + y
</syntaxhighlight>

=== 文档注释 ===
文档注释使用<code>/--</code>开头，用于生成API文档：
<syntaxhighlight lang="lean">
/-- 计算两个自然数之和 -/
def add (x y : Nat) := x + y
</syntaxhighlight>

== 嵌套注释 ==
Lean支持'''嵌套注释'''，这在临时注释掉包含注释的代码块时特别有用：
<syntaxhighlight lang="lean">
/-
外层注释
  /- 内层注释 -/
-/
</syntaxhighlight>

== 实际应用案例 ==

=== 案例1：代码说明 ===
<syntaxhighlight lang="lean">
/--
将华氏温度转换为摄氏温度
* `f`：华氏温度值
* 返回：对应的摄氏温度
-/
def fahrenheitToCelsius (f : Float) : Float :=
  (f - 32) * 5 / 9  -- 标准转换公式
</syntaxhighlight>

=== 案例2：调试辅助 ===
<syntaxhighlight lang="lean">
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

/-
暂时禁用优化版本进行调试
def factorial (n : Nat) : Nat :=
  match n with
  | 0 => 1
  | m + 1 => (m + 1) * factorial m
-/
</syntaxhighlight>

== 注释与证明 ==
在Lean定理证明中，注释常用于解释证明步骤：
<syntaxhighlight lang="lean">
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero =>
    -- 基本情况：0 + b = b + 0
    simp
  | succ a ih =>
    -- 归纳步骤：(a + 1) + b = b + (a + 1)
    simp [Nat.add_succ, Nat.succ_add, ih]
</syntaxhighlight>

== 最佳实践 ==

* 为每个顶层定义添加文档注释
* 使用注释解释复杂的算法逻辑
* 避免显而易见的注释
* 临时注释代码时注明原因和日期
* 保持注释与代码同步更新

== 注释与工具链 ==
Lean的文档工具会解析文档注释生成HTML文档。例如：
<mermaid>
graph LR
    A[.lean文件] --> B[文档注释提取]
    B --> C[文档生成器]
    C --> D[HTML文档]
</mermaid>

== 数学公式注释 ==
当注释中包含数学公式时：
<math>
/-- 勾股定理：a² + b² = c² -/
</math>

== 注释风格指南 ==
{| class="wikitable"
|-
! 注释类型 !! 建议使用场景
|-
| 单行注释 || 简短说明、行内注释
|-
| 多行注释 || 复杂算法说明、临时禁用代码
|-
| 文档注释 || 模块、定理和函数说明
|}

== 总结 ==
Lean注释是代码不可或缺的组成部分，良好的注释习惯可以：
* 提高代码可读性
* 辅助团队协作
* 生成专业文档
* 简化调试过程

合理使用各种注释类型，将使你的Lean项目更易于理解和维护。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean基础]]