13.1. 标识符🔗

语法标识符

$x:ident

标识符项是对名称的引用。标识符的具体词法语法见 Lean 具体语法一节。标识符也会出现在绑定名称的上下文中，例如 Lean.Parser.Term.let : termlet 和 Lean.Parser.Term.fun : termfun；不过，这些绑定位置本身并不是完整的项。标识符到名称的映射并不简单：在模块中的任意位置，都可能打开了若干命名空间，还可能存在节变量和局部绑定。此外，标识符可以包含多个由点分隔的原子标识符；点既用于分隔命名空间与其内容，也用于分隔变量与采用字段表示法的字段或函数。这会产生歧义，因为标识符 A.B.C.D.e.f 可能指下列任一含义：

命名空间 A.B.C.D.e 中的名称 f（例如，在 e 的 Lean.Parser.Command.declaration : commandwhere 块中定义的函数）
若 A.B.C.D.e 的类型为 T，则是将 T.f 应用于 A.B.C.D.e
从名为 A.B.C.D.e 的结构中投影字段 f
从结构值 A 依次投影字段 B.C.D.e，再用字段表示法应用 f
若命名空间 Q 已打开，则可能指上述任一带 Q 前缀的含义，例如命名空间 Q.A.B.C.D.e 中的名称 f

此列表并不穷尽所有可能。给定一个标识符，精译器必须找出它指向哪个或哪些名称，并判断末尾的组成部分中是否有字段，或通过字段表示法应用的函数。这称为对名称进行解析。

全局环境中的某些声明会在首次被引用时惰性创建。若解析标识符的过程既创建了这样的声明，又得到对它的引用，就称为实现该名称。名称解析与名称实现遵循相同规则，因此本节虽只提及名称解析，但内容同时适用于二者。

名称解析受以下因素影响：

附加到标识符上的预解析名称
附加到标识符上的宏作用域
作用域内的局部绑定，包括精译 Lean.Parser.Term.letrec : termlet rec 时创建的辅助定义
当前模块传递导入的模块中用 Lean.Parser.Command.export : commandexport 创建的别名
当前节作用域，尤其是当前命名空间、已打开的命名空间和节变量

标识符的任意前缀都可能解析为一组名称。未参与解析过程的后缀随后会被视为字段投影或字段表示法。较长前缀的解析优先于较短前缀；换言之，标识符中应尽可能少地把组成部分视为字段表示法。标识符前缀可以指下列任一项，越靠前者优先级越高：

名称（包括宏作用域）与标识符前缀相同的局部绑定变量；较近的局部绑定优先于外层局部绑定
名称与标识符前缀相同的局部辅助定义
名称与标识符前缀相同的节变量
与“当前命名空间的某个前缀加上标识符前缀”相同的全局名称，或在当前命名空间的某个前缀中存在别名的全局名称；当前命名空间的较长前缀优先于较短前缀
通过 Lean.Parser.Command.open : commandopen 命令引入作用域、且与标识符前缀相同的全局名称

若标识符解析为多个名称，精译器会尝试使用其中每一个。若恰好只有一个成功，就将其作为该标识符的含义。若成功者不止一个，或全部失败，都会报错。

局部名称优先

局部绑定优先于全局绑定：

def x := "global"

"local"#eval
  let x := "local"
  x

"local"

名称最内层的局部绑定优先于其他绑定：

"inner"#eval
  let x := "outer"
  let x := "inner"
  x

"inner"

在线查看 ↪

当前命名空间的较长前缀优先

命名空间 A、B 和 C 相互嵌套。 A 和 C 都包含 x 的定义。

namespace A
def x := "A.x"
namespace B
namespace C
def x := "A.B.C.x"

当前命名空间为 A.B.C 时，x 解析为 A.B.C.x。

"A.B.C.x"#eval x

"A.B.C.x"

当前命名空间为 A.B 时，x 解析为 A.x。

end C
"A.x"#eval x

"A.x"

在线查看 ↪

较长的标识符前缀优先

当标识符可能指从不同名称进行的投影时，名称最长者优先：

structure A where
  y : String
deriving Repr

structure B where
  y : A
deriving Repr

def y : B := ⟨⟨"shorter"⟩⟩
def y.y : A := ⟨"longer"⟩

给定上述声明，y.y.y 原则上既可指 y 的 y 字段的 y 字段，也可指 y.y 的 y 字段。它指 y.y 的 y 字段，因为名称 y.y 是 y.y.y 比名称 y 更长的前缀：

"longer"#eval y.y.y

"longer"

在线查看 ↪

当前命名空间的内容优先于已打开的命名空间

当标识符既可能指当前命名空间某个前缀中定义的名称，也可能指已打开命名空间中的名称时，前者优先。

namespace A
def x := "A.x"
end A

namespace B
def x := "B.x"
namespace C
open A
"B.x"#eval x

尽管打开 A 的时间晚于 B.x 的声明，标识符 x 仍解析为 B.x 而非 A.x，因为 B 是当前命名空间 B.C 的前缀。

"B.x"#eval x

"B.x"

在线查看 ↪

有歧义的标识符

在此例中，x 既可能指 A.x，也可能指 B.x，且二者都不优先。由于二者类型相同，因此会报错。

def A.x := "A.x"
def B.x := "B.x"
open A
open B
#eval Ambiguous term
  x
Possible interpretations:
  B.x : String
  
  A.x : Stringx

Ambiguous term
  x
Possible interpretations:
  B.x : String
  
  A.x : String

通过类型消歧

当原本有歧义的名称类型不同时，会利用类型消除歧义：

def C.x := "C.x"
def D.x := 3
open C
open D
"C.x"#eval (x : String)

"C.x"

在线查看 ↪

13.1.1. 前导 `.`🔗

当标识符以点（.）开头时，会使用精译器对表达式的预期类型来解析它，而不是使用当前命名空间和已打开命名空间的集合。广义字段表示法与此相关：这种前导点表示法使用标识符的预期类型将其解析为名称，而字段表示法使用紧邻点之前的项的推断类型。

带前导 . 的标识符会在预期类型的命名空间中查找。若项的预期类型是应用于零个或多个实参的常量，则其命名空间就是该常量的名称。若该类型不是常量的应用（例如函数、元变量或宇宙），则它没有命名空间。

若在预期类型的命名空间中找不到该名称，但展开这个常量能得到另一常量，则转而查找后者的命名空间。重复此过程，直到遇到并非常量应用的内容，或常量无法继续展开为止。

前导 .

.replicate 的预期类型是 List Unit。该类型的命名空间是 List，因此 .replicate 解析为 List.replicate。

[(), (), ()]#eval show List Unit from .replicate 3 ()

[(), (), ()]

在线查看 ↪

前导 . 与展开定义

.replicate 的预期类型是 MyList Unit。该类型的命名空间是 MyList，但不存在定义 MyList.replicate。展开 MyList Unit 得到 List Unit，因此 .replicate 解析为 List.replicate。

def MyList α := List α
[(), (), ()]#eval show MyList Unit from .replicate 3 ()

[(), (), ()]

在线查看 ↪

13.1. 标识符🔗

13.1.1. 前导 .🔗

13.1.1. 前导 `.`🔗