diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index b3db109198..1423d04e48 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -553,7 +553,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L | some (baseStructName, fullName) => pure $ LValResolution.const baseStructName structName fullName | none => throwLValError e eType - m!"invalid field notation, '{fieldName}' is not a valid \"field\" because the environment does not contain '{Name.mkStr structName fieldName}'" + m!"invalid field '{fieldName}', the environment does not contain '{Name.mkStr structName fieldName}'" -- search local context first, then environment let searchCtx : Unit → TermElabM LValResolution := fun _ => do let fullName := Name.mkStr structName fieldName diff --git a/tests/lean/346.lean b/tests/lean/346.lean index 4c82f55d96..2c1be47853 100644 --- a/tests/lean/346.lean +++ b/tests/lean/346.lean @@ -8,3 +8,6 @@ def a : SomeType := SomeType.x end SomeType #eval SomeType.b + +def f (x : Nat) := + x.z diff --git a/tests/lean/346.lean.expected.out b/tests/lean/346.lean.expected.out index ca33ac24e9..b94c90e5b0 100644 --- a/tests/lean/346.lean.expected.out +++ b/tests/lean/346.lean.expected.out @@ -1,3 +1,7 @@ 346.lean:10:6-10:16: error: unknown constant 'SomeType.b' 346.lean:10:0-10:16: error: failed to synthesize Lean.Eval ?m +346.lean:13:2-13:5: error: invalid field 'z', the environment does not contain 'Nat.z' + x +has type + Nat