diff --git a/tests/elabissues/anonymous_constructor_error_msg.lean b/tests/elabissues/anonymous_constructor_error_msg.lean new file mode 100644 index 0000000000..ede12c5d08 --- /dev/null +++ b/tests/elabissues/anonymous_constructor_error_msg.lean @@ -0,0 +1,22 @@ +/- +This is an annoyingly unhelpful error message that I see all the time. +An exact line number would help a lot, but even so it would be great +to replace the `⟨...⟩` with the actual term in question. +-/ +structure Foo := (n : Nat) + +def Foo.sum (xs : List Foo) : Foo := +xs.foldl (λ s x => ⟨s.n + x.n⟩) ⟨0⟩ + +#check +let x1 := ⟨1⟩; +let x2 := ⟨2⟩; +let x3 := ⟨3⟩; +let x4 := ⟨4⟩; +let x5 := ⟨5⟩; +let x6 := ⟨6⟩; +Foo.sum [x1, x2, x3, x5, x6] +/- +error: invalid constructor ⟨...⟩, expected type is not an inductive type + ?m_1 +-/ diff --git a/tests/elabissues/invalid_field_notation_error_msg.lean b/tests/elabissues/invalid_field_notation_error_msg.lean new file mode 100644 index 0000000000..1f86f3bc60 --- /dev/null +++ b/tests/elabissues/invalid_field_notation_error_msg.lean @@ -0,0 +1,19 @@ +/- +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. +-/ +structure Foo := (n : Nat) +def Foo.f1 (f : Foo) : Nat := f.n +def Foo.f2 (f : Foo) : Nat := f.n +def Foo.f3 (f : Foo) : Nat := f.n +def Foo.f4 (f : Foo) : Nat := f.n +def Foo.f5 (f : Foo) : Nat := f.n + +#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 +-/