From 36ea3fbaf7b4b20ff84379f410bfb4b2f46138c1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 18 Feb 2020 10:49:04 -0800 Subject: [PATCH] doc: document issue cc @dselsam --- tests/elabissues/invalid_field_notation_error_msg.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tests/elabissues/invalid_field_notation_error_msg.lean b/tests/elabissues/invalid_field_notation_error_msg.lean index 1f86f3bc60..ca83821d81 100644 --- a/tests/elabissues/invalid_field_notation_error_msg.lean +++ b/tests/elabissues/invalid_field_notation_error_msg.lean @@ -2,6 +2,11 @@ This is an annoyingly unhelpful error message that I see frequently. It reports the prefix of the field notation, but not the field that we are trying to access. An exact line number would help, but even so it would be great to report the field as well. + +[Leo]: the bad line number is due to the transition from Lean3 to Lean4. +The new frontend reports the exact position. It still fails to elaborate since +the types of `f`, `g` and `h` are unknown, and there is no `Foo.f6`. +I decided to no report the field, users have all information they neeed when the correct position is reported. -/ structure Foo := (n : Nat) def Foo.f1 (f : Foo) : Nat := f.n @@ -10,10 +15,13 @@ def Foo.f3 (f : Foo) : Nat := f.n def Foo.f4 (f : Foo) : Nat := f.n def Foo.f5 (f : Foo) : Nat := f.n +new_frontend + #check (λ f g h => let x : Foo := ⟨f.n + 1⟩; let y : Foo := ⟨g.n + 1⟩; (λ f g h => f.f1 + g.f2 + h.f3 + f.f4 + g.f5 + h.f6) f g h) + /- /home/dselsam/omega/lean4/tests/elabissues/invalid_field_notation_error.lean:8:0: error: invalid field notation, type is not of the form (C ...) where C is a constant -/