关于：`invalidField`🔗

Error code: lean.invalidField

Generalized field notation used in a potentially ambiguous way.

Severity: ErrorSince: 4.22.0

此错误表明遇到了包含点后跟标识符的表达式，并且不可能将标识符理解为一个字段。

Lean 的字段表示法非常强大，但这也会使其变得混乱：表达式 color.value 可以是单个标识符。它可以是对结构体字段的引用，并且它并且是对值 color 调用函数通用字段表示法。

示例🔗

Incorrect Field Name

#eval (4 + 2).Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression
  4 + 2
of type `Nat`suc

Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression
  4 + 2
of type `Nat`

6#eval (4 + 1).succ

无效字段错误的最简单原因是正在寻找的函数，例如 Nat.suc，不存在。

Projecting from the Wrong Expression

#eval '>'.Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression
  '>'
of type `Char`leftpad 10 ['a', 'b', 'c']

Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression
  '>'
of type `Char`

['>', '>', '>', '>', '>', '>', '>', 'a', 'b', 'c']#eval ['a', 'b', 'c'].leftpad 10 '>'

点之前表达式的类型完全决定了该字段调用的函数投影。不存在 Char.leftpad，并且使用通用调用 List.leftpad 的唯一方法字段表示法是将列表放在点之前。

Type is Not Specific

def double_plus_one {α} [Add α] (x : α) :=
   Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  x + x
has type `α` which does not have the necessary form.(x + x).succ

Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  x + x
has type `α` which does not have the necessary form.

def double_plus_one (x : Nat) :=
   (x + x).succ

Add 类型类足以执行加法 x + x，但 .succ 字段表示法如果不了解更多有关 succ 所投影的实际类型的信息，则无法进行操作。

Insufficient Type Information

example := fun (n) => Invalid field notation: Type of
  n
is not known; cannot resolve field `succ`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Fin.succ`
  • `Nat.succ`
  • `Lean.Level.succ`
  • `Std.PRange.succ`
  • `Lean.Level.PP.Result.succ`
  • `Std.Time.Internal.Bounded.LE.succ`n.succ.succ

Invalid field notation: Type of
  n
is not known; cannot resolve field `succ`

Hint: Consider replacing the field projection with a call to one of the following:
  • `Fin.succ`
  • `Nat.succ`
  • `Lean.Level.succ`
  • `Std.PRange.succ`
  • `Lean.Level.PP.Result.succ`
  • `Std.Time.Internal.Bounded.LE.succ`

example := fun (n : Nat) => n.succ.succ

仅当可以确定正在使用的类型时才能使用通用字段表示法预计。可能需要添加 Type 注释才能使通用字段表示法起作用。

关于：invalidField🔗

示例🔗

关于：`invalidField`🔗