Lean 语言参考手册

23.1. 自定义运算符🔗

Lean 支持自定义中缀、前缀和后缀运算符。 任何 Lean 库都可以添加新运算符，而这些新运算符与语言内置运算符具有同等地位。 每个新运算符都会被赋予一个作为函数的解释，随后对该运算符的使用会被翻译为对该函数的使用。 运算符到函数调用的这种翻译被称为它的 展开。 如果这个函数是某个 类型类 方法，那么就可以通过定义该类的实例来重载生成的运算符。

所有运算符都有一个 优先级。 运算符优先级决定了无括号表达式中的运算顺序：由于乘法的优先级高于加法，2 + 3 * 4 等价于 2 + (3 * 4)，而 2 * 3 + 4 等价于 (2 * 3) + 4。 中缀运算符还具有一个 结合性，它决定了同一优先级的一串运算符应如何理解：

左结合

这类运算符向左嵌套。 加法是左结合的，因此 2 + 3 + 4 + 5 等价于 ((2 + 3) + 4) + 5。

右结合

这类运算符向右嵌套。 积类型是右结合的，因此 Nat × String × Unit × Option Int 等价于 Nat × (String × (Unit × Option Int))。

非结合

将这类运算符串接起来会导致语法错误。 必须显式加括号。 等号是非结合的，因此下面的写法是错误的：

1 + 2 = 3 expected end of input= 2 + 1

解析器错误为：

<example>:1:10-1:11: expected end of input
前缀与中缀运算符的优先级

命题 ¬A ∧ B 等价于 (¬A) ∧ B，因为 ¬ 的优先级高于 ∧。 由于 ∧ 的优先级高于 =，并且它是右结合的，所以 ¬A ∧ B = (¬A) ∧ B 等价于 ¬A ∧ ((B = ¬A) ∧ B)。

在线查看 ↪

Lean 提供了用于定义新运算符的命令：

语法运算符声明

非结合中缀运算符使用 Lean.Parser.Command.mixfix : commandinfix 定义：

command ::= ...
    | docComment?
      attributes?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind infix:prec ((name := ident))? ((priority := prio))? str => term

左结合中缀运算符使用 Lean.Parser.Command.mixfix : commandinfixl 定义：

command ::= ...
    | docComment?
      attributes?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind infixl:prec ((name := ident))? ((priority := prio))? str => term

右结合中缀运算符使用 Lean.Parser.Command.mixfix : commandinfixr 定义：

command ::= ...
    | docComment?
      attributes?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind infixr:prec ((name := ident))? ((priority := prio))? str => term

前缀运算符使用 Lean.Parser.Command.mixfix : commandprefix 定义：

command ::= ...
    | docComment?
      attributes?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind prefix:prec ((name := ident))? ((priority := prio))? str => term

后缀运算符使用 Lean.Parser.Command.mixfix : commandpostfix 定义：

command ::= ...
    | docComment?
      attributes?
      `attrKind` 匹配 `("scoped" <|> "local")?`，用于属性之前，例如 `@[local simp]`。attrKind postfix:prec ((name := ident))? ((priority := prio))? str => term

这些命令前面都可以带有 文档注释 和 属性。 当用户将鼠标悬停在运算符上时，会显示该文档注释；而属性则和其他任何声明一样，可以调用任意元程序。 inherit_doc 属性会让实现该运算符的函数的文档被复用于运算符本身。

运算符与 节作用域 的交互方式和属性相同。 默认情况下，运算符在任何传递导入了其定义所在模块的模块中都可用；但也可以将其声明为 scoped 或 local，分别把可用范围限制为当前命名空间已被打开的上下文，或者当前的 节作用域。

自定义运算符需要在冒号后提供一个 优先级 说明。 自定义运算符没有可回退使用的默认优先级。

运算符也可以显式命名。 这个名字表示对 Lean 语法的扩展，主要用于元编程。 如果没有显式提供名字，Lean 会根据运算符自动生成一个。 不应依赖这个名字的具体分配方式，因为内部命名算法可能改变，而且上游依赖中引入相似运算符也可能造成冲突；在这种情况下，Lean 会修改所分配的名字，直到它唯一为止。

自动分配的运算符名称

给定这个中缀运算符：

infix:90 " ⤴ " => Option.getD

生成的解析器扩展会被赋予内部名称 «term_⤴_»。

在线查看 ↪
显式提供的运算符名称

给定这个中缀运算符：

infix:90 (name := getDOp) " ⤴ " => Option.getD

生成的解析器扩展会命名为 getDOp。

在线查看 ↪
继承文档

给定这个中缀运算符：

@[inherit_doc] infix:90 " ⤴ " => Option.getD

生成的解析器扩展具有与 Option.getD 相同的文档。

在线查看 ↪

当定义了多个共享同一语法的运算符时，Lean 的解析器会尝试它们全部。 如果有多个成功，就会选择消耗输入最多的那个——这被称为 局部最长匹配规则。 在某些情况下，多个运算符的解析都可能成功，并且它们覆盖的是输入中的同一范围。 这时会使用运算符的 优先权 来选择合适的结果。 最后，如果多个同优先权运算符在最长匹配上并列，解析器就会保留所有结果，并由精译器逐个尝试；如果不能恰好有一个成功精译，则整体失败。

歧义运算符与优先权

将 + 的另一种实现定义为 Or 只需要一条中缀运算符声明。

infix:65 " + " => Or

有了这个声明，Lean 在精译加法时会同时尝试使用 HAdd.hAdd 的内置语法和 Or 的新语法：

True + False : Prop#check True + False 
True + False : Prop
2 + 2 : Nat#check 2 + 2 
2 + 2 : Nat

不过，由于这个新运算符不是结合的，局部最长匹配规则 意味着只有 HAdd.hAdd 能应用于不加括号的三参数写法：

#check failed to synthesize instance of type class HAdd Prop Prop ?m.3 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.True + False + True 
failed to synthesize instance of type class
  HAdd Prop Prop ?m.3

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

如果把这个中缀运算符声明为高优先权，那么在有歧义的情况下 Lean 就不会尝试内置的 HAdd.hAdd 运算符：

infix:65 (priority := high) " + " => Or True + False : Prop#check True + False 
True + False : Prop
sorry + sorry : Prop#check failed to synthesize instance of type class OfNat Prop 2 numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is Prop due to the absence of the instance above Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.2 + failed to synthesize instance of type class OfNat Prop 2 numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is Prop due to the absence of the instance above Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.2 
failed to synthesize instance of type class
  OfNat Prop 2
numerals are polymorphic in Lean, but the numeral `2` cannot be used in a context where the expected type is
  Prop
due to the absence of the instance above

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

这个新运算符不是结合的，因此 局部最长匹配规则 意味着只有 HAdd.hAdd 能应用于三参数写法：

#check failed to synthesize instance of type class HAdd Prop Prop ?m.3 Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.True + False + True 
failed to synthesize instance of type class
  HAdd Prop Prop ?m.3

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

实际的运算符以字符串字面量给出。 新运算符必须满足下列要求：

  • 它至少必须包含一个字符。

  • 第一个字符不能是单引号或双引号（' 或 "），除非运算符本身是 ''。

  • 它不能以反引号（`）开头，后面也不能紧跟一个可作为引用名称合法前缀的字符。

  • 它不能以数字开头。

  • 它不能包含内部空白。

运算符字符串字面量可以以空格开头或结尾。 这些空格不属于运算符语法的一部分，它们的存在也不会要求在使用运算符时必须在两侧留空格。 不过，空格的存在会使 Lean 在向用户显示运算符时插入空格。 省略这些空格会让运算符参数在显示时紧贴运算符本身。

最后，运算符的含义通过 Lean.Parser.Command.mixfix : command=> 给出，并与运算符本身分隔开。 这里可以是任意 Lean 项。 对运算符的使用会被解糖为函数应用，并把给定项放在函数位置。 前缀和后缀运算符会把该项应用到自己的单个显式参数上。 中缀运算符则会按顺序把该项应用到左参数和右参数上。 除了要能在每个使用点接收参数之外，对这个项没有其他特殊要求。 运算符可以构造函数，因此这个项可以期待比运算符更多的参数。 隐式参数和 实例隐式 参数会在每个应用点被解析，这使得运算符可以由某个 类型类 方法 来定义。

如果这个项要么是全局环境中的一个名称，要么是这样一个名称对一个或多个参数的应用，那么 Lean 会自动为该运算符生成一个 逆展开器。 这意味着，凡是原本会显示相应函数项的地方，运算符都会显示在 Lean 的 证明状态、错误消息和其他输出中。 Lean 不会跟踪原始项里是否真的使用了该运算符；只要有机会，它就会把它插入进去。

Lean 输出中的自定义运算符

函数 perhapsFactorial 会在数字不太大时计算它的阶乘。

def fact : Nat → Nat | 0 => 1 | n+1 => (n + 1) * fact n def perhapsFactorial (n : Nat) : Option Nat := if n < 8 then some (fact n) else none

可以用后缀惊叹问号运算符来表示它。

postfix:90 "‽" => perhapsFactorial

在尝试证明 ∀ n, n ≥ 8 → (perhapsFactorial n).isNone 时，初始证明状态会使用这个新运算符，尽管定理原文并没有这样写：

⊢ ∀ (n : Nat), n ≥ 8 → n‽.isNone = true
在线查看 ↪
中缀运算符、已定义函数与逆展开器

当运算符不会展开成对某个已定义函数的应用时，就不会生成逆展开器。 这里，后缀惊叹问号会展开成一个匿名函数：当参数不太大时，它会取其阶乘。

def fact : Nat → Nat | 0 => 1 | n+1 => (n + 1) * fact n set_option quotPrecheck false in postfix:90 "‽" => fun (n : Nat) => if n < 8 then some (fact n) else none

由于展开式中没有具名函数，因此无法生成逆展开器：

(fun n => if n < 8 then some (fact n) else none) 7 : Option Nat#check 7‽ 
(fun n => if n < 8 then some (fact n) else none) 7 : Option Nat

使用具名函数则会产生一个逆展开器，它会用于那些由 perhapsFactorial 的应用构成的项：

def perhapsFactorial (n : Nat) : Option Nat := if n < 8 then some (fact n) else none postfix:90 "‽'" => perhapsFactorial 7‽' : Option Nat#check 7‽' 
7‽' : Option Nat
在线查看 ↪