指令(commands) / 顶层交互指令(top-level interactive commands)
它们不是用于定义定理/函数的核心逻辑代码，而是为了辅助开发、调试和交互，比如查看类型、求值、打印信息等，仅在交互式环境，如 Lean 编辑器、VS Code 插件中生效，编译时会被忽略。
常见Lean 4指令：
| 指令 | 作用 | 实例 |
|---|---|---|
#check | 查看任意表达式、变量、定理、函数的类型 | #check 123 -- Output: 123 : Nat |
#eval | 执行表达式并打印其运行时结果 | #eval 10 + 20 * 3 -- Output：70 |
#print | 展示函数、定理、类型的完整实现/定义 | def square (n : Nat) : Nat := n * n#print square -- Ouput：def square : Nat → Nat := fun (n : Nat) => n * n |
#reduce | 将表达式完全展开到最基础的形式，适合理解复杂表达式的本质。 | def double (n : Nat) : Nat := n + n#reduce double 5 -- Output：5 + 5（展开 double 的定义，而非直接算 10）#eval double 5 -- Output：10（直接计算结果） |
#exit | 终止当前 Lean 会话（仅 REPL 中生效） | |
#help | 查看所有可用指令的帮助信息 | |
#lint | 检查当前文件中的代码风格/常见错误（需导入 Std.Tactic.Lint） | |
#synth | 自动推导类型类实例（如#synth Decidable (5 > 3)） | |
#where | 查看当前上下文的变量/假设 |
注意事项：
-
#指令是交互式专属的：仅在 Lean 的交互环境中有效，如果你写的是编译为可执行文件的 Lean 代码，这些指令会被编译器忽略，不会影响最终程序。 -
区分
#指令和@/!：-
#是顶层交互指令（全局生效）； -
@用于显式指定类型类实例 / 忽略自动推导； -
!常用于战术（tactic）的 “强制” 版本（如rw!）。
-
-
作用域：
#指令通常写在文件的顶层（函数 / 定理外），少数（如#where）可写在证明块内。
Lean 4中的类型
- 将值集合组合在一起的类型（如结构
Structure）称为 积类型（Product Types） - 允许选择的数据类型称为 和类型（Sum Types）
- 可以包含自身实例的数据类型称为 递归数据类型（Recursive Datatypes）
- 递归和类型称为 归纳数据类型（Inductive Datatypes）
Bool类型就是归纳数据类型：inductive Bool where | false : Bool | true : Bool