2 days ago
- Lean 使用 `:=` 进行定义，`=` 进行比较，并对 `String`、`Nat`、`Int` 进行类型推断。
- `#eval` 运行代码并在 InfoView 中显示结果，而 `#print` 可以输出到终端。
- 证明使用 `theorem` 编写，并采用诸如 `unfold`、`decide`、`simp` 和 `omega` 等策略。
- 函数调用不使用括号或逗号：`f a b c`；括号仅用于分组表达式。
- `let` 绑定允许在函数内部进行局部定义，最后一个表达式是返回值。
- 函数可以通过多种方式声明，具有显式或隐式类型，包括匿名 `fun` 语法。
- 全称量词 `∀` 能够证明参数所有可能取值的命题。
- 隐式参数 `{ }` 和实例参数 `[ ]` 由 Lean 自动填充，减少了样板代码。
- Lean 具有高度交互性：在任意标识符上使用 `Command+Click` 可打开其定义或源代码。