编辑“︁Lean常见困难”︁（章节）

== 类型系统与依赖类型 ==  
Lean 的核心特性是依赖类型系统，这可能导致以下问题：

=== 类型推断困惑 ===  
初学者常因依赖类型的复杂性而难以理解类型推断规则。例如：
<syntaxhighlight lang="lean">
def double (x : Nat) : Nat := x + x
#check double  -- 输出：Nat → Nat
</syntaxhighlight>
此处 `double` 的类型为 `Nat → Nat`，但若错误地尝试应用于非 `Nat` 类型：
<syntaxhighlight lang="lean">
#check double "hello"  -- 类型错误！
</syntaxhighlight>
'''解决方法'''：使用 `#print` 命令检查定义细节，或通过 `set_option trace.Meta.synthInstance true` 启用类型推断追踪。

=== 依赖类型匹配 ===  
依赖模式匹配可能导致非直观的行为。例如定义向量长度函数：
<syntaxhighlight lang="lean">
inductive Vec (α : Type) : Nat → Type where
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

def head : Vec α (n + 1) → α
  | cons x xs => x  -- 无法处理 `nil` 情况！
</syntaxhighlight>
'''关键点'''：Lean 会强制检查所有可能的依赖模式，需使用「不可能模式」标记：
<syntaxhighlight lang="lean">
def head : Vec α (n + 1) → α
  | cons x xs => x
  | nil => nomatch n  -- 显式排除 n ≠ 0 的情况
</syntaxhighlight>