`lean.invalidField`

Dotted identifier notation used without .

Severity: ErrorSince: 4.22.0

This error indicates that an expression containing a dot followed by an identifier was encountered, and that it wasn't possible to understand the identifier as a field.

Lean's field notation is very powerful, but this can also make it confusing: the expression color.value can either be a single identifier, it can be a reference to the field of a structure, and it and be a calling a function on the value color with generalized field notation.

Examples

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

The simplest reason for an invalid field error is that the function being sought, like Nat.suc, does not exist.

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 '>'

The type of the expression before the dot entirely determines the function being called by the field projection. There is no Char.leftpad, and the only way to invoke List.leftpad with generalized field notation is to have the list come before the dot.

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

The Add typeclass is sufficient for performing the addition x + x, but the .succ field notation cannot operate without knowing more about the actual type from which succ is being projected.

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`
  • `Std.PRange.succ`n.succ.succ

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

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

Generalized field notation can only be used when it is possible to determine the type that is being projected. Type annotations may need to be added to make generalized field notation work.