关于：`invalidField`🔗

Error code: lean.invalidField

Generalized field notation used in a potentially ambiguous way.

Severity: ErrorSince: 4.22.0

此错误表示遇到了包含点号后跟标识符的表达式，但无法将该标识符理解为字段。

Lean 的字段表示法非常强大，但这也可能令人困惑：表达式 color.value 可以是单个标识符，也可以是对结构体字段的引用，还可以使用广义字段表示法对值 color 调用函数。

示例🔗

错误的字段名称

#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）不存在。

从错误表达式投影

#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 的唯一方式是让列表出现在点号之前。

类型不够具体

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，否则无法工作。

类型信息不足

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

只有能够确定被投影的类型时，才能使用广义字段表示法。可能需要添加类型注解，才能使广义字段表示法正常工作。

关于：invalidField🔗

示例🔗

关于：`invalidField`🔗