关于：`unknownIdentifier`🔗

Error code: lean.unknownIdentifier

Failed to resolve identifier to variable or constant.

Severity: ErrorSince: 4.23.0

此错误意味着 Lean 无法找到与给定名称匹配的变量或常量。更多准确地说，这意味着无法解析该名称，如手册部分中所述标识符：不将输入解释为局部变量或节变量的名称（如果适用）、先前声明的全局常量或前述任何一项的预测都是有效的。（“如果适用”是指在某些情况下案例 - 例如，Lean.Parser.Command.print : command#print 命令的参数 - 名称已解析仅适用于全局常量。）

请注意，此错误消息将仅显示标识符的一种可能的解析，但出现此错误表示它可能引用的所有可能的名称均失败。对于例如，如果在命名空间 A 和 B 打开的情况下输入标识符 x，则错误消息“未知标识符 `x`”表示找不到 x、A.x 或 B.x 中的任何一个（或 A.x 或 B.x（如果存在）是受保护的声明）。

导致此错误的常见原因包括忘记导入定义常量的模块，当命名空间未打开时省略常量的命名空间，或尝试引用本地变量 variable that is not in scope.

为了帮助解决其中一些常见问题，此错误消息附带了一个代码操作，该操作建议与所提供的名称类似的常量名称。这些包括环境中的常数以及可以从其他模块导入的内容。请注意，这些建议可用仅通过受支持的代码编辑器的内置代码操作机制，而不是作为错误中的提示消息本身。

示例🔗

Variable Not in Scope

example (s : IO.FS.Stream) := do
  IO.withStdout s do
    let text := "Hello"
    IO.println text
  IO.println s!"Wrote '{Unknown identifier `text`text}' to stream"

Unknown identifier `text`

example (s : IO.FS.Stream) := do
  let text := "Hello"
  IO.withStdout s do
    IO.println text
  IO.println s!"Wrote '{text}' to stream"

此示例的最后一行出现未知标识符错误，因为变量 text 是不在范围内。第三行的 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.do : termdo 块，不能在外部 Lean.Parser.Term.do : termdo 块中访问。将此绑定移动到外部 Lean.Parser.Term.do : termdo 块——它仍然存在也在内部块的范围内——解决了这个问题。

Missing Namespace

inductive Color where
  | rgb (r g b : Nat)
  | grayscale (k : Nat)

def red : Color :=
  Unknown identifier `rgb`rgb 255 0 0

Unknown identifier `rgb`

inductive Color where
  | rgb (r g b : Nat)
  | grayscale (k : Nat)

def red : Color :=
  Color.rgb 255 0 0

inductive Color where
  | rgb (r g b : Nat)
  | grayscale (k : Nat)

open Color in
def red : Color :=
  rgb 255 0 0

在此示例中，最后一行的标识符 rgb 不会解析为 Color 构造函数那个名字的。这是因为构造函数的名称实际上是 Color.rgb： inductive type have names in that type's namespace. Because the Color namespace is not open, the 如果没有命名空间前缀，则无法使用标识符 rgb。

解决此错误的一种方法是提供完全限定的构造函数名称 Color.rgb；的也可以使用点标识符符号 .rgb，因为 .rgb 255 0 0 的预期类型是 Color。或者，可以打开 Color 命名空间并继续省略 Color 前缀来自标识符。

Protected Constant Name Without Namespace Prefix

protected def A.x := ()

open A

example := Unknown identifier `x`x

Unknown identifier `x`

protected def A.x := ()

open A

example := A.x

protected def A.x := ()

open A (x)

example := x

在此示例中，由于常量 A.x 为 protected，因此不能通过后缀引用它 x 即使命名空间 A 打开。因此，标识符 x 无法解析。相反，要引用 protected 常量时，必须至少包含其最内部的命名空间 - 在此案例，A。或者，限制打开语法 - 在第二个更正的示例中演示示例—允许通过其非限定名称引用 protected 常量，而无需打开它发生的命名空间的其余部分（请参阅手册部分命名空间和部分了解详细信息）。

Unresolvable Name Inferred by Dotted-Identifier Notation

def disjoinToNat (b₁ b₂ : Bool) : Nat :=
  Unknown constant `Nat.toNat`

Note: Inferred this name from the expected resulting type of `.toNat`:
  Nat.toNat (b₁ || b₂)

Unknown constant `Nat.toNat`

Note: Inferred this name from the expected resulting type of `.toNat`:
  Nat

def disjoinToNat (b₁ b₂ : Bool) : Nat :=
  (b₁ || b₂).toNat

def disjoinToNat (b₁ b₂ : Bool) : Nat :=
  Bool.toNat (b₁ || b₂)

在此示例中，点标识符符号 .toNat 导致 Lean 推断出无法解析的名称 (Nat.toNat)。点标识符表示法使用的命名空间总是从它出现的表达式的预期类型，由于类型注释 disjoinToNat—在此示例中为 Nat。使用参数类型的命名空间——作为作者这段代码似乎是有意的——使用通用字段表示法，如第一个更正的代码所示示例。或者，可以通过编写完整的名称空间来明确指定正确的名称空间限定函数名称。

Auto-bound variables

set_option relaxedAutoImplicit false in
def thisBreaks (x : α₁) (y : Unknown identifier `size₁`

Note: It is not possible to treat `size₁` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.size₁) := ()

set_option autoImplicit false in
def thisAlsoBreaks (x : Unknown identifier `α₂`

Note: It is not possible to treat `α₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.α₂) (y : Unknown identifier `size₂`

Note: It is not possible to treat `size₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.size₂) := ()

Unknown identifier `size₁`

Note: It is not possible to treat `size₁` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`.

set_option relaxedAutoImplicit true in
def thisWorks (Variable name `x` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`x : α₁) (Variable name `y` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`y : size₁) := ()

set_option autoImplicit true in
def thisAlsoWorks (Variable name `x` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`x : α₂) (Variable name `y` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`y : size₂) := ()

set_option relaxedAutoImplicit false in
def thisWorks {size₁} (Variable name `x` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`x : α₁) (Variable name `y` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`y : size₁) := ()

set_option autoImplicit false in
def thisAlsoWorks {α₂ size₂} (Variable name `x` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`x : α₂) (Variable name `y` is not explicitly referenced.

The binding can be removed (if unused) or named `_` (if used implicitly).

Note: This linter can be disabled with `set_option linter.unusedVariables false`y : size₂) := ()

Lean 的默认行为，当它遇到无法在 a 类型中识别的标识符时定义，就是添加自动隐式参数对于那些未知的标识符。然而，许多文件或项目通过设置禁用此功能 autoImplicit 或 relaxedAutoImplicit 选项至 false。

无需重新启用 autoImplicit 或 relaxedAutoImplicit 选项，最简单的方法修复此错误的方法是将未知标识符添加为普通隐式参数如上例所示。

关于：unknownIdentifier🔗

示例🔗

关于：`unknownIdentifier`🔗