编辑“︁Lean常用快捷键”︁

= Lean常用快捷键 =

== 介绍 ==  
Lean 是一款强大的交互式定理证明器，广泛用于形式化数学和编程验证。掌握其快捷键可以显著提升开发效率，特别是在频繁切换证明状态和浏览代码时。本页面将详细介绍 Lean 中常用的快捷键及其应用场景，适合初学者和进阶用户参考。

== 基础导航快捷键 ==  
以下快捷键适用于 Lean 的默认编辑器（如 VS Code 或 Emacs 插件）：

{| class="wikitable"  
|+ 基础导航快捷键表  
! 快捷键 !! 功能 !! 说明  
|-  
| <code>Ctrl + Enter</code> || 执行当前行或选中代码 || 在 Lean 中触发类型检查或证明推进  
|-  
| <code>Alt + ↑/↓</code> || 上下移动代码块 || 调整证明步骤的顺序  
|-  
| <code>Ctrl + .</code> || 跳转到定义 || 查看函数或定理的定义  
|-  
| <code>Ctrl + Shift + .</code> || 查找引用 || 定位符号的使用位置  
|-  
| <code>F12</code> || 重命名符号 || 重构时修改变量或定理名称  
|}  

== 证明交互快捷键 ==  
在编写证明时，以下快捷键尤为实用：

=== 补全建议 ===  
* <code>Ctrl + Space</code>：触发自动补全（如输入 <code>rw</code> 后补全 <code>rewrite</code>）。  
* <code>Tab</code>：在补全菜单中选择建议项。

=== 证明辅助 ===  
* <code>Ctrl + Alt + Enter</code>：尝试自动填充证明（如使用 <code>simp</code> 或 <code>auto</code>）。  
* <code>Ctrl + /</code>：注释/取消注释当前行。

<syntaxhighlight lang="lean">  
-- 示例：使用快捷键快速补全  
example : 2 + 2 = 4 := by  
  simp -- 输入 `simp` 后按 Ctrl+Enter 执行  
</syntaxhighlight>  

== 高级编辑技巧 ==  
=== 多光标操作 ===  
* <code>Alt + Click</code>：添加多个光标。  
* <code>Ctrl + D</code>：选中当前单词并查找下一个相同项。

=== 代码折叠 ===  
* <code>Ctrl + Shift + [</code>：折叠当前代码块。  
* <code>Ctrl + Shift + ]</code>：展开代码块。

== 实际案例 ==  
以下是一个使用快捷键优化证明流程的示例：

<syntaxhighlight lang="lean">  
-- 初始证明（手动输入）  
theorem add_comm (a b : Nat) : a + b = b + a := by  
  induction a  
  · simp  
  · simp [Nat.succ_add, *]  

-- 使用快捷键优化后：  
-- 1. 输入 `induction a` 后按 Ctrl+Enter 执行  
-- 2. 按 Alt+↓ 移动第二个 `simp` 到正确位置  
-- 3. 使用 Ctrl+/ 注释掉未完成的步骤  
</syntaxhighlight>  

== 快捷键图示 ==  
<mermaid>  
flowchart TD  
    A[开始编写证明] --> B[输入策略如 simp]  
    B --> C{Ctrl+Enter执行}  
    C --> D[查看目标状态]  
    D --> E[继续编辑或补全]  
</mermaid>  

== 数学公式支持 ==  
快捷键效率提升的量化分析：  
<math>  
\text{节省时间} = \sum_{i=1}^{n} (t_{\text{手动}} - t_{\text{快捷键}})  
</math>  

== 总结 ==  
熟练掌握 Lean 的快捷键可以大幅减少重复操作时间，尤其适合长证明或大型项目。建议从基础导航开始练习，逐步适应高级编辑功能。

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