13.1. 标识符🔗

$x:ident

标识符术语是对名称的引用。标识符的具体词法语法在 有关 Lean 的具体语法的部分中进行了描述。 标识符也出现在绑定名称的上下文中，例如 Lean.Parser.Term.let : term`let` is used to declare a local definition. Example: ``` let x := 1 let y := x + 1 x + y ``` Since functions are first class citizens in Lean, you can use `let` to declare local functions too. ``` let double := fun x => 2*x double (double 3) ``` For recursive definitions, you should use `let rec`. You can also perform pattern matching using `let`. For example, assume `p` has type `Nat × Nat`, then you can write ``` let (x, y) := p x + y ``` The *anaphoric let* `let := v` defines a variable called `this`. let 和 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 的应用

• 字段 f 从名为 A.B.C.D.e 的结构的投影

• 根据结构值 A 进行一系列字段投影 B.C.D.e，然后使用字段表示法应用 f

• 如果命名空间 Q 已打开，则它可能是对以上任何带有 Q 前缀的引用，例如命名空间 Q.A.B.C.D.e 中的名称 f

此列表并不详尽。 给定标识符，精化器必须发现标识符引用的是哪个名称或哪些名称，以及任何尾随组件是否是通过字段表示法应用的字段或函数。 这个名字叫做resolving。

全局环境中的一些声明是在第一次引用时延迟创建的。 以创建这些声明之一并导致对其引用的方式解析标识符称为 realizing 名称。 解析和实现名称的规则是相同的，因此即使本节仅涉及解析名称，它也适用于两者。

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

• 预解析名称 附加到标识符

• 附加到标识符的 宏范围

• 范围内的本地绑定，包括作为 Lean.Parser.Term.letrec : termlet rec 的精化的一部分创建的辅助定义。

• 在当前模块传递导入的模块中使用 Lean.Parser.Command.export : commandAdds names from other namespaces to the current namespace. The command `export Some.Namespace (name₁ name₂)` makes `name₁` and `name₂`: - visible in the current namespace without prefix `Some.Namespace`, like `open`, and - visible from outside the current namespace `N` as `N.name₁` and `N.name₂`. ## Examples ```lean namespace Morning.Sky def star := "venus" end Morning.Sky namespace Evening.Sky export Morning.Sky (star) -- `star` is now in scope #check star end Evening.Sky -- `star` is visible in `Evening.Sky` #check Evening.Sky.star ``` export 创建的别名

• 当前的 节范围，特别是 当前命名空间、打开的命名空间和节变量

标识符的任何前缀都可以解析为一组名称。 然后，未包含在解析过程中的后缀将被视为场投影或场符号。 较长前缀的解析优先于较短前缀的解析；换句话说，尽可能少的标识符组成部分被视为字段符号。 标识符前缀可以指以下任何一项，较早的项目优先于后面的项目：

1. 名称与标识符前缀相同的本地绑定变量，包括宏作用域，更接近的本地绑定优先于外部本地绑定。

2. 名称与标识符前缀相同的本地辅助定义

3. 名称与标识符前缀相同的 节变量

4. 与附加到标识符前缀的 当前命名空间 前缀相同的全局名称，或者当前命名空间的前缀中存在别名，当前命名空间的较长前缀优先于较短前缀

5. 已通过 Lean.Parser.Command.open : commandMakes names from other namespaces visible without writing the namespace prefix. Names that are made available with `open` are visible within the current `section` or `namespace` block. This makes referring to (type) definitions and theorems easier, but note that it can also make [scoped instances], notations, and attributes from a different namespace available. The `open` command can be used in a few different ways: * `open Some.Namespace.Path1 Some.Namespace.Path2` makes all non-protected names in `Some.Namespace.Path1` and `Some.Namespace.Path2` available without the prefix, so that `Some.Namespace.Path1.x` and `Some.Namespace.Path2.y` can be referred to by writing only `x` and `y`. * `open Some.Namespace.Path hiding def1 def2` opens all non-protected names in `Some.Namespace.Path` except `def1` and `def2`. * `open Some.Namespace.Path (def1 def2)` only makes `Some.Namespace.Path.def1` and `Some.Namespace.Path.def2` available without the full prefix, so `Some.Namespace.Path.def3` would be unaffected. This works even if `def1` and `def2` are `protected`. * `open Some.Namespace.Path renaming def1 → def1', def2 → def2'` same as `open Some.Namespace.Path (def1 def2)` but `def1`/`def2`'s names are changed to `def1'`/`def2'`. This works even if `def1` and `def2` are `protected`. * `open scoped Some.Namespace.Path1 Some.Namespace.Path2` **only** opens [scoped instances], notations, and attributes from `Namespace1` and `Namespace2`; it does **not** make any other name available. * `open <any of the open shapes above> in` makes the names `open`-ed visible only in the next command or expression. [scoped instance]: https://lean-lang.org/theorem_proving_in_lean4/type_classes.html#scoped-instances (Scoped instances in Theorem Proving in Lean) ## Examples ```lean /-- SKI combinators https://en.wikipedia.org/wiki/SKI_combinator_calculus -/ namespace Combinator.Calculus def I (a : α) : α := a def K (a : α) : β → α := fun _ => a def S (x : α → β → γ) (y : α → β) (z : α) : γ := x z (y z) end Combinator.Calculus section -- open everything under `Combinator.Calculus`, *i.e.* `I`, `K` and `S`, -- until the section ends open Combinator.Calculus theorem SKx_eq_K : S K x = I := rfl end -- open everything under `Combinator.Calculus` only for the next command (the next `theorem`, here) open Combinator.Calculus in theorem SKx_eq_K' : S K x = I := rfl section -- open only `S` and `K` under `Combinator.Calculus` open Combinator.Calculus (S K) theorem SKxy_eq_y : S K x y = y := rfl -- `I` is not in scope, we have to use its full path theorem SKxy_eq_Iy : S K x y = Combinator.Calculus.I y := rfl end section open Combinator.Calculus renaming I → identity, K → konstant #check identity #check konstant end section open Combinator.Calculus hiding S #check I #check K end section namespace Demo inductive MyType | val namespace N1 scoped infix:68 " ≋ " => BEq.beq scoped instance : BEq MyType where beq _ _ := true def Alias := MyType end N1 end Demo -- bring `≋` and the instance in scope, but not `Alias` open scoped Demo.N1 #check Demo.MyType.val == Demo.MyType.val #check Demo.MyType.val ≋ Demo.MyType.val -- #check Alias -- unknown identifier 'Alias' end ``` open 命令纳入范围的全局名称，与标识符前缀相同

如果标识符解析为多个名称，则精化器尝试使用所有这些名称。 如果其中一个成功，则将其用作标识符的含义。 如果多个成功或全部失败，则为错误。

"local"

"inner"

"A.B.C.x"

"A.x"

"longer"

"B.x"

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

"C.x"

[(), (), ()]

[(), (), ()]