The Lean Language Reference

About: invalidField

Error code: 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` • `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

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.