6. 与 Lean 交互
你现在已经熟悉了依值类型论的基本原理，它既是一种定义数学对象的语言，也是一种构造证明的语言。 现在你缺少一个定义新数据类型的机制。下一章介绍 归纳数据类型 的概念来帮你完成这个目标。 但首先，在这一章中，我们从类型论的机制中抽身出来，探索与 Lean 交互的一些实用性问题。
并非所有的知识都能马上对你有用。可以略过这一节，然后在必要时再回到这一节以了解 Lean 的特性。
6.1. 消息
Lean 产生三种消息：
- 错误 (Errors)
当代码中的不一致意味着无法处理时，就会产生错误。例如语法错误（例如缺少
)）和类型错误（例如试图将自然数加到函数上）。
- 警告 (Warnings)
警告描述了代码的潜在问题，例如存在
sorry。与错误不同，代码并非毫无意义；但是，警告值得仔细关注。
- 信息 (Information)
信息并不表示代码有任何问题，包括
#check和#eval等命令的输出。
Lean 可以检查命令是否产生预期的消息。如果消息匹配，则忽略任何错误；这可用于确保发生正确的错误。
如果不匹配，则会产生错误。你可以使用 #guard_msgs 命令来指示预期的消息。
这是一个例子：
/--
error: Type mismatch
"Not a number"
has type
String
but is expected to have type
Nat
-/
#guard_msgs in
def x : Nat := "Not a number"
在 #guard_msgs 后的括号中包含消息类别会导致它仅检查指定的类别，而让其他类别通过。
在此示例中，#eval 由于存在 sorry 而发出错误，但通常针对 sorry 发出的警告照常显示：
/--
error: aborting evaluation since the expression depends on the
'sorry' axiom, which can lead to runtime instability and crashes.
To attempt to evaluate anyway despite the risks, use the '#eval!'
command.
-/
#guard_msgs(error) in
#eval (sorry : Nat)如果没有配置，则会捕获这两条消息：
/--
error: aborting evaluation since the expression depends on the
'sorry' axiom, which can lead to runtime instability and crashes.
To attempt to evaluate anyway despite the risks, use the '#eval!'
command.
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
#eval (sorry : Nat)
本书中的一些示例使用 #guard_msgs 来指示预期的错误。
6.2. 导入文件
Lean 的前端的目标是解释用户的输入，构建形式化的表达式，并检查它们是否形式良好和类型正确。 Lean 还支持使用各种编辑器，这些编辑器提供持续的检查和反馈。更多信息可以在 Lean 文档上找到。
Lean 的标准库中的定义和定理分布在多个文件中。用户也可能希望使用额外的库，或在多个文件中开发自己的项目。
当 Lean 启动时，它会自动导入库中 Init 文件夹的内容，其中包括一些基本定义和结构。
因此，我们在这里介绍的大多数例子都是“开箱即用”的。
然而，如果你想使用其他文件，需要通过文件开头的 import 语句手动导入。命令
importBar.Baz.Blah
导入文件 Bar/Baz/Blah.olean，其中的描述是相对于 Lean 搜索路径 解释的。
关于如何确定搜索路径的信息可以在文档中找到。
默认情况下，它包括标准库目录，以及（在某些情况下）用户的本地项目的根目录。
导入是传递性的。换句话说，如果你导入了 Foo，并且 Foo 导入了 Bar，
那么你也可以访问 Bar 的内容，而不需要明确导入它。
6.3. 小节（续）
Lean 提供了各种分段机制来帮助构造理论。你在 变量和小节 中看到，
section 命令不仅可以将理论中的元素组合在一起，还可以在必要时声明变量，作为定理和定义的参数插入。
请记住，variable 命令的意义在于声明变量，以便在定理中使用，如下面的例子：
section
variable (x y : Nat)
def double := x + x
#check double y
#check double (2 * x)
attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm
theorem t1 : double (x + y) = double x + double y := x:Naty:Nat⊢ double (x + y) = double x + double y
All goals completed! 🐙
#check t1 y
#check t1 (2 * x)
theorem t2 : double (x * y) = double x * y := x:Naty:Nat⊢ double (x * y) = double x * y
All goals completed! 🐙
end
double 的定义不需要声明 x 作为参数；Lean 检测到这种依赖关系并自动插入。
同样，Lean 检测到 x 在 t1 和 t2 中的出现，也会自动插入。
注意，double 没有 y 作为参数。变量只包括在实际使用的声明中。
6.4. 命名空间（续）
在 Lean 中，标识符是由层次化的 名称 给出的，如 Foo.Bar.baz。
我们在 命名空间 一节中看到，Lean 提供了处理分层名称的机制。
命令 namespace Foo 导致 Foo 被添加到每个定义和定理的名称中，直到遇到 end Foo。
命令 open Foo 然后为以 Foo 开头的定义和定理创建临时的 别名 。
下面的定义
def Foo.bar : Nat := 1
被看成一个宏，展开成
尽管定理和定义的名称必须是唯一的，但标识它们的别名却不是。当我们打开一个命名空间时，一个标识符可能是模糊的。
Lean 试图使用类型信息来消除上下文中的含义，但你总是可以通过给出全名来消除歧义。
为此，字符串 _root_ 是对空前缀的明确表述。
def String.add (a b : String) : String :=
a ++ b
def Bool.add (a b : Bool) : Bool :=
a != b
def add (α β : Type) : Type := Sum α β
open Bool
open String
-- This reference is ambiguous:
-- #check add
#check String.add
#check Bool.add
#check _root_.add
#check add "hello" "world"
#check add true false
#check add Nat Nat
我们可以通过使用 protected 关键字来阻止创建较短的别名：
protected def Foo.bar : Nat := 1
open Foo
/-- error: Unknown identifier `bar` -/
#guard_msgs in
#check bar -- error
#check Foo.bar
这通常用于像 Nat.rec 和 Nat.recOn 这样的名称，以防止普通名称的重载。
open 命令允许变体。命令
仅对列出的标识符创建了别名。命令
open Nat hiding succ gcd
#check zero
/-- error: Unknown identifier `gcd` -/
#guard_msgs in
#eval gcd 15 6 -- error
#eval Nat.gcd 15 6
给 Nat 命名空间中 除了 被列出的标识符都创建了别名。
将 Nat.mul 更名为 times，Nat.add 更名为 plus。
有时，将别名从一个命名空间 export 到另一个命名空间，或者导出到顶层是很有用的。命令
在当前命名空间中为 succ、add 和 sub 创建别名，
这样无论何时命名空间被打开，这些别名都可以使用。如果这个命令在名字空间之外使用，那么这些别名会被输出到顶层。
6.5. 属性
Lean 的主要功能是把用户的输入翻译成形式化的表达式，由内核检查其正确性，然后存储在环境中供以后使用。
但是有些命令对环境有其他的影响，或者给环境中的对象分配属性，定义符号，或者声明类型类的实例，
如 类型类 一章所述。这些命令大多具有全局效应，也就是说，它们不仅在当前文件中保持有效，
而且在任何导入它的文件中也保持有效。然而，这类命令通常支持 local 修饰符，
这表明它们只在当前 section 或 namespace 关闭前或当前文件结束前有效。
在 使用简化器 一节中，我们看到可以用 [simp] 属性来注释定理，
这使它们可以被简化器使用。下面的例子定义了列表的前缀关系，证明了这种关系是自反的，并为该定理分配了 [simp] 属性。
def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
∃ t, l₁ ++ t = l₂
@[simp] theorem List.isPrefix_self (as : List α) : isPrefix as as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
example : isPrefix [1, 2, 3] [1, 2, 3] := ⊢ isPrefix [1, 2, 3] [1, 2, 3]
All goals completed! 🐙
然后简化器通过将其改写为 True 来证明 isPrefix [1, 2, 3] [1, 2, 3]。
你也可以在做出定义后的任何时候分配属性：
theorem List.isPrefix_self (as : List α) : isPrefix as as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
attribute [simp] List.isPrefix_self
在所有这些情况下，该属性在任何导入该声明的文件中仍然有效。添加 local 修饰符可以限制范围：
section
theorem List.isPrefix_self (as : List α) : isPrefix as as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
attribute [local simp] List.isPrefix_self
example : isPrefix [1, 2, 3] [1, 2, 3] := ⊢ isPrefix [1, 2, 3] [1, 2, 3]
All goals completed! 🐙
end
/-- error: `simp` made no progress -/
#guard_msgs in
example : isPrefix [1, 2, 3] [1, 2, 3] := ⊢ isPrefix [1, 2, 3] [1, 2, 3]
⊢ isPrefix [1, 2, 3] [1, 2, 3]
另一个例子，我们可以使用 instance 命令来给 isPrefix 关系分配符号 ≤。
该命令将在 类型类 一章中解释，它的工作原理是给相关定义分配一个 [instance] 属性。
def isPrefix (l₁ : List α) (l₂ : List α) : Prop :=
∃ t, l₁ ++ t = l₂
instance : LE (List α) where
le := isPrefix
theorem List.isPrefix_self (as : List α) : as ≤ as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
这个分配也可以是局部的：
def instLe : LE (List α) :=
{ le := isPrefix }
section
attribute [local instance] instLe
example (as : List α) : as ≤ as :=
⟨[], α:Type u_1as:List α⊢ as ++ [] = as All goals completed! 🐙⟩
end
/--
error: failed to synthesize
LE (List α)
Hint: Additional diagnostic information may be available using the
`set_option diagnostics true` command.
-/
#guard_msgs in
example (as : List α) : as ≤ as :=
⟨[], by simp⟩
在下面的 符号 一节中，我们将讨论 Lean 定义符号的机制，并看到它们也支持 local 修饰符。
然而，在 设置选项 一节中，我们将讨论 Lean 设置选项的机制，它并 不 遵循这种模式：
选项 只能 在局部设置，也就是说，它们的范围总是限制在当前小节或当前文件中。
6.6. 隐参数（续）
在 隐参数 一节中，我们看到，如果 Lean 将术语 t 的类型显示为 {x : α} → β x，
那么大括号表示 x 被标记为 t 的 隐参数。这意味着每当你写 t 时，就会插入一个占位符，
或者说“洞”，这样 t 就会被 @t _ 取代。如果你不希望这种情况发生，你必须写 @t 来代替。
请注意，隐参数是急于插入的。假设我们定义一个函数 f : (x : Nat) → {y : Nat} → (z : Nat) → Nat。
那么，当我们写表达式 f 7 时，没有进一步的参数，它会被解析为 @f 7 _。
Lean 提供了一个较弱的注释，它指定了一个占位符只应在后一个显式参数 之前 添加。
这个注释可以用双大括号写，所以 f 的类型是 f : (x : Nat) → {{y : Nat}} → (z : Nat) → Nat。
有了这个注释，表达式 f 7 将被解析为原样，而 f 7 3 将被解析为 @f 7 _ 3，就像使用强注释一样。
这个注释也可以写成 ⦃y : Nat⦄，其中的 Unicode 括号输入方式为 \{{ 和 \}}。
为了说明这种区别，请看下面的例子，它表明一个自反的欧几里得关系既是对称的又是传递的。
def reflexive {α : Type u} (r : α → α → Prop) : Prop :=
∀ (a : α), r a a
def symmetric {α : Type u} (r : α → α → Prop) : Prop :=
∀ {a b : α}, r a b → r b a
def transitive {α : Type u} (r : α → α → Prop) : Prop :=
∀ {a b c : α}, r a b → r b c → r a c
def Euclidean {α : Type u} (r : α → α → Prop) : Prop :=
∀ {a b c : α}, r a b → r a c → r b c
theorem th1 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: symmetric r :=
fun {a b : α} =>
fun (h : r a b) =>
show r b a from euclr h (reflr _)
theorem th2 {α : Type u} {r : α → α → Prop}
(symmr : symmetric r) (euclr : Euclidean r)
: transitive r :=
fun {a b c : α} =>
fun (rab : r a b) (rbc : r b c) =>
euclr (symmr rab) rbc
theorem th3 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: transitive r :=
th2 (th1 reflr @euclr) @euclr
variable (r : α → α → Prop)
variable (euclr : Euclidean r)
#check euclr
这些结果被分解成几个小步骤：th1 表明自反和欧氏的关系是对称的，th2 表明对称和欧氏的关系是传递的。
然后 th3 结合这两个结果。但是请注意，我们必须手动禁用 euclr 中的隐参数，
否则会插入太多的隐参数。如果我们使用弱隐式参数，这个问题就会消失：
def reflexive {α : Type u} (r : α → α → Prop) : Prop :=
∀ (a : α), r a a
def symmetric {α : Type u} (r : α → α → Prop) : Prop :=
∀ {{a b : α}}, r a b → r b a
def transitive {α : Type u} (r : α → α → Prop) : Prop :=
∀ {{a b c : α}}, r a b → r b c → r a c
def Euclidean {α : Type u} (r : α → α → Prop) : Prop :=
∀ {{a b c : α}}, r a b → r a c → r b c
theorem th1 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: symmetric r :=
fun {a b : α} =>
fun (h : r a b) =>
show r b a from euclr h (reflr _)
theorem th2 {α : Type u} {r : α → α → Prop}
(symmr : symmetric r) (euclr : Euclidean r)
: transitive r :=
fun {a b c : α} =>
fun (rab : r a b) (rbc : r b c) =>
euclr (symmr rab) rbc
theorem th3 {α : Type u} {r : α → α → Prop}
(reflr : reflexive r) (euclr : Euclidean r)
: transitive r :=
th2 (th1 reflr euclr) euclr
variable (r : α → α → Prop)
variable (euclr : Euclidean r)
#check euclr
还有第三种隐式参数，用方括号表示，[ 和 ]。这些是用于类型类的，在 类型类 一章中解释。
6.7. 符号
Lean 中的标识符可以包含任何字母数字字符，包括希腊字符（除了 ∀、Σ 和 λ，正如我们所见，它们在依值类型论中具有特殊含义）。
它们还可以包含下标，可以通过键入 \_ 后跟所需的下标字符来输入。
Lean 的解析器是可扩展的，也就是说，我们可以定义新的符号。
Lean 的语法可以由用户在各个层面上进行扩展和自定义，从基本的“混合（mixfix）”符号到自定义阐述器。 事实上，所有内置语法都是使用向用户开放的相同机制和 API 进行解析和处理的。在本节中，我们将描述和解释各种扩展点。
虽然引入新符号在编程语言中是一个相对罕见的功能，有时甚至因为可能使代码变得晦涩难懂而不被看好， 但在形式化中，它是一个无价的工具，可以简洁地在代码中表达相关领域既定的约定和符号。 除了基本符号之外，Lean 能够将常见的样板代码分解为（行为良好的）宏，并嵌入整个自定义领域特定语言（DSL）， 以高效且可读地对子问题进行文本编码，这对程序员和证明工程师都大有裨益。
6.7.1. 符号和优先级
最基本的语法扩展命令允许引入新的（或重载现有的）前缀、中缀和后缀运算符。
infixl:65 " + " => HAdd.hAdd -- left-associative
infix:50 " = " => Eq -- non-associative
infixr:80 " ^ " => HPow.hPow -- right-associative
prefix:100 "-" => Neg.neg
postfix:max "⁻¹" => Inv.inv
在描述运算符种类（其“固定性”）的初始命令名称之后，我们给出运算符的 解析优先级，
前面加冒号 :，然后是用双引号括起来的新标记或现有标记（空格用于漂亮打印），
然后是箭头 => 之后该运算符应转换为的函数。
优先级是一个自然数，描述运算符与其参数绑定的“紧密”程度，编码运算顺序。 我们可以通过查看上面展开的命令来更精确地说明这一点：
notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs
notation:50 lhs:51 " = " rhs:51 => Eq lhs rhs
notation:80 lhs:81 " ^ " rhs:80 => HPow.hPow lhs rhs
notation:100 "-" arg:100 => Neg.neg arg
-- `max` is a shorthand for precedence 1024:
notation:1024 arg:1024 "⁻¹" => Inv.inv arg
事实证明，第一个代码块中的所有命令实际上都是命令 宏，它们转换为更通用的 notation 命令。
我们将在下面学习编写此类宏。notation 命令不接受单个标记，而是接受标记和具有优先级的命名项占位符的混合序列，
这些占位符可以在 => 的右侧引用，并将被在该位置解析的相应项替换。优先级为 p 的占位符在该位置仅接受优先级至少为 p 的符号。
因此，字符串 a + b + c 不能解析为等同于 a + (b + c)，因为 infixl 符号的右侧操作数的优先级比符号本身大 1。
相比之下，infixr 对右侧操作数重用符号的优先级，因此 a ^ b ^ c 可以 解析为 a ^ (b ^ c)。
请注意，如果我们直接使用 notation 引入中缀符号，例如
其中优先级不足以确定结合性，Lean 的解析器将默认为右结合。更准确地说，
在存在歧义语法的情况下，Lean 的解析器遵循局部 最长解析 规则：当解析 a ~ b ~ c 中的 a ~ 的右侧时，
它将尽可能长时间地继续解析（只要当前优先级允许），不会在 b 之后停止，而是也会解析 ~ c。
因此，该项等同于 a ~ (b ~ c)。
如上所述，notation 命令允许我们定义任意 混合 语法，自由混合标记和占位符。
set_option quotPrecheck false
notation:max "(" e ")" => e
notation:10 Γ " ⊢ " e " : " τ => Typing Γ e τ
没有优先级的占位符默认为 0，即它们在其位置接受任何优先级的符号。
如果两个符号重叠，我们再次应用最长解析规则：
新符号优于二元符号，因为后者在链接之前会在 1 + 2 之后停止解析。
如果有多个符号接受相同的最长解析，则选择将推迟到阐述阶段，除非恰好有一个重载是类型正确的，否则阐述将失败。
6.8. 强制转换
在 Lean 中，自然数的类型 Nat，与整数的类型 Int 不同。
但是有一个函数 Int.ofNat 将自然数嵌入整数中，这意味着我们可以在需要时将任何自然数视为整数。
Lean 有机制来检测和插入这种 强制转换。可以使用重载的 ↑ 运算符显式请求强制转换。
6.9. 显示信息
有很多方法可以让你查询 Lean 的当前状态以及当前上下文中可用的对象和定理的信息。
你已经看到了两个最常见的方法，#check 和 #eval。
请记住，#check 经常与 @ 运算符一起使用，它使定理或定义的所有参数显式化。
此外，你可以使用 #print 命令来获得任何标识符的信息。
如果标识符表示一个定义或定理，Lean 会打印出符号的类型，以及它的定义。
如果它是一个常数或公理，Lean 会指出它并显示其类型。
6.10. 设置选项
Lean 维护着一些内部变量，用户可以通过设置这些变量来控制其行为。语法如下：
set_option <name> <value>
有一系列非常有用的选项可以控制 Lean 的 美观打印（pretty printer） 显示项的方式。下列选项的输入值为 true 或 false：
pp.explicit : display implicit arguments pp.universes : display hidden universe parameters pp.notation : display output using defined notations
例如，以下设置会产生更长的输出：
set_option pp.explicit true
set_option pp.universes true
set_option pp.notation false
#check 2 + 2 = 4
#reduce (fun x => x + 2) = (fun x => x + 3)
#check (fun x => x + 1) 1
命令 set_option pp.all true 一次性执行这些设置，
而 set_option pp.all false 则恢复到之前的值。
当你调试一个证明，或试图理解一个神秘的错误信息时，美观打印额外的信息往往是非常有用的。
不过太多的信息可能会让人不知所措，Lean 的默认值一般来说对普通的交互是足够的。
6.11. 使用库
为了有效地使用 Lean，你将不可避免地需要使用库中的定义和定理。
回想一下，文件开头的 import 命令会从其他文件中导入之前编译的结果，而且导入是传递的；
如果你导入了 Foo，Foo 又导入了 Bar，那么 Bar 的定义和定理也可以被你利用。
但是打开一个命名空间的行为，提供了更短的名字，并没有延续下去。在每个文件中，你需要打开你想使用的命名空间。
一般来说，你必须熟悉库和它的内容，这样你就知道有哪些定理、定义、符号和资源可供你使用。 下面我们将看到 Lean 的编辑器模式也可以帮助你找到你需要的东西，但直接研究库的内容往往是不可避免的。 Lean 的标准库在 GitHub 上：
你可以使用 GitHub 的浏览器界面查看这些目录和文件的内容。如果你在自己的电脑上安装了 Lean，
你可以在 lean 文件夹中找到这个库，用你的文件管理器探索它。每个文件顶部的注释标题提供了额外的信息。
Lean 库的开发者遵循一般的命名准则，以便于猜测你所需要的定理的名称，
或者在支持 Lean 模式的编辑器中用 Tab 自动补全来找到它，这将在下一节讨论。
标识符一般是 camelCase，而类型是 CamelCase。
对于定理的名称，我们依靠描述性的名称，其中不同的组成部分用 _ 分开。
通常情况下，定理的名称只是描述结论：
请记住，Lean 中的标识符可以组织成层次化的命名空间。
例如，命名空间 Nat 中名为 le_of_succ_le_succ 的定理的全名是 Nat.le_of_succ_le_succ，
但是通过命令 open Nat 可以使用更短的名称（对于未标记为 protected 的名称）。
我们将在 归纳类型 和 结构体和记录 章节中看到，
在 Lean 中定义结构体和归纳数据类型会生成相关的操作，这些操作存储在与定义类型同名的命名空间中。
例如，乘积类型带有以下操作：
第一个用于构造对，而接下来的两个 Prod.fst 和 Prod.snd 投影这两个元素。
最后一个 Prod.rec 提供了另一种机制，用于根据两个分量上的函数定义乘积上的函数。
像 Prod.rec 这样的名称是 受保护的（protected），这意味着即使打开了 Prod 命名空间，也必须使用全名。
根据命题即类型对应关系，逻辑连接词也是归纳类型的实例，因此我们也倾向于对它们使用点符号：
6.12. 自动绑定隐式参数
在上一节中，我们展示了隐式参数如何使函数使用起来更方便。
然而，像 compose 这样的函数定义起来仍然相当冗长。
请注意，宇宙多态的 compose 甚至比之前定义的那个还要冗长。
universe u v w
def compose {α : Type u} {β : Type v} {γ : Type w}
(g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
你可以通过在定义 compose 时提供宇宙参数来避免使用 universe 命令。
def compose.{u, v, w}
{α : Type u} {β : Type v} {γ : Type w}
(g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
Lean 4 支持一项名为 自动绑定隐式参数 的新功能。它使得像 compose 这样的函数编写起来更加方便。
当 Lean 处理声明的头部时，任何未绑定的标识符都会自动添加为隐式参数。有了这个功能，我们可以将 compose 写为：
请注意，Lean 使用 Sort 而不是 Type 推断出了更通用的类型。
虽然我们喜欢这个功能并在实现 Lean 时广泛使用它，但我们意识到一些用户可能会对此感到不舒服。
因此，你可以使用命令 set_option autoImplicit false 禁用它。
set_option autoImplicit false
/--
error: Unknown identifier `β`
---
error: Unknown identifier `γ`
---
error: Unknown identifier `α`
---
error: Unknown identifier `β`
---
error: Unknown identifier `α`
---
error: Unknown identifier `γ`
-/
#guard_msgs in
def compose (g : β → γ) (f : α → β) (x : α) : γ :=
g (f x)
6.13. 隐式 Lambda
当表达式的预期类型是等待隐式参数的函数时，阐述器会自动引入相应的 lambda。
例如，pure 的类型表明第一个参数是隐式类型 α，
但 ReaderT.pure 的第一个参数是 reader monad 的上下文类型 ρ。
它会自动被 fun {α} => ... 包围，这允许阐述器正确填充主体中的隐式参数。
instance : Monad (ReaderT ρ m) where
pure := ReaderT.pure
bind := ReaderT.bind
用户可以通过使用 @ 或编写带有 {} 或 [] 绑定器注释的 lambda 表达式来禁用隐式 lambda 功能。
这里有几个例子：
set_option linter.unusedVariables false
namespace Ex2
def id1 : {α : Type} → α → α :=
fun x => x
def listId : List ({α : Type} → α → α) :=
(fun x => x) :: []
-- In this example, implicit lambda introduction has been disabled because
-- we use `@` before {kw}`fun`
-- 在此示例中，隐式 lambda 引入已被禁用，因为我们在 {kw}`fun` 之前使用了 `@`
def id2 : {α : Type} → α → α :=
@fun α (x : α) => id1 x
def id3 : {α : Type} → α → α :=
@fun α x => id1 x
def id4 : {α : Type} → α → α :=
fun x => id1 x
-- In this example, implicit lambda introduction has been disabled
-- because we used the binder annotation `{...}`
-- 在此示例中，隐式 lambda 引入已被禁用，因为我们使用了绑定器注释 `{...}`
def id5 : {α : Type} → α → α :=
fun {α} x => id1 x
end Ex2
6.14. 简单函数的语法糖
Lean 包含一种使用匿名占位符而不是 fun 来描述简单函数的符号。
当 · 作为项的一部分出现时，最近的封闭括号将成为一个以 · 为参数的函数。
如果括号包含多个占位符而没有其他中间括号，则它们将从左到右成为参数。这里有几个例子：
namespace Ex3
#check (· + 1)
#check (2 - ·)
#eval [1, 2, 3, 4, 5].foldl (· * ·) 1
def f (x y z : Nat) :=
x + y + z
#check (f · 1 ·)
#eval [(1, 2), (3, 4), (5, 6)].map (·.1)end Ex3
嵌套括号引入新函数。在下面的示例中，创建了两个不同的 lambda 表达式：
6.15. 命名参数
命名参数允许你通过将参数与其名称匹配而不是与其在参数列表中的位置匹配来指定参数的实参。 如果你不记得参数的顺序但知道它们的名称，你可以以任何顺序发送参数。 当 Lean 无法推断隐式参数时，你也可以为其提供值。 命名参数还通过标识每个参数代表的内容来提高代码的可读性。
def sum (xs : List Nat) :=
xs.foldl (init := 0) (·+·)
#eval sum [1, 2, 3, 4]-- 10
example {a b : Nat} {p : Nat → Nat → Nat → Prop}
(h₁ : p a b b) (h₂ : b = a) :
p a a b :=
Eq.subst (motive := fun x => p a x b) h₂ h₁
在下面的示例中，我们说明了命名参数和默认参数之间的交互。
def f (x : Nat) (y : Nat := 1) (w : Nat := 2) (z : Nat) :=
x + y + w - z
example (x z : Nat) : f (z := z) x = x + 1 + 2 - z := rfl
example (x z : Nat) : f x (z := z) = x + 1 + 2 - z := rfl
example (x y : Nat) : f x y = fun z => x + y + 2 - z := rfl
example : f = (fun x z => x + 1 + 2 - z) := rfl
example (x : Nat) : f x = fun z => x + 1 + 2 - z := rfl
example (y : Nat) : f (y := 5) = fun x z => x + 5 + 2 - z := rfl
def g {α} [Add α] (a : α) (b? : Option α := none) (c : α) : α :=
match b? with
| none => a + c
| some b => a + b + c
variable {α} [Add α]
example : g = fun (a c : α) => a + c := rfl
example (x : α) : g (c := x) = fun (a : α) => a + x := rfl
example (x : α) : g (b? := some x) = fun (a c : α) => a + x + c := rfl
example (x : α) : g x = fun (c : α) => x + c := rfl
example (x y : α) : g x y = fun (c : α) => x + y + c := rfl
你可以使用 .. 将缺失的显式参数作为 _ 提供。
此功能与命名参数结合使用对于编写模式非常有用。这里有一个例子：
inductive Term where
| var (name : String)
| num (val : Nat)
| app (fn : Term) (arg : Term)
| lambda (name : String) (type : Term) (body : Term)
def getBinderName : Term → Option String
| Term.lambda (name := n) .. => some n
| _ => none
def getBinderType : Term → Option Term
| Term.lambda (type := t) .. => some t
| _ => none
当 Lean 可以自动推断显式参数，并且我们希望避免一连串的 _ 时，省略号也很有用。