Floris van Doorn

Ok, then feel free to close it.

Oh, I think that would be a great improvement, and might indeed solve all the problems this RFC is trying to solve.

One issue that is not be solved by your suggestion is when you have a (non-unsolved goal) error in your declaration. That can still be easy to miss. And certain...

Yes, I think most of this issue has been resolved. I haven't played with Lean much yet this month, but I have one remark: Would it be possible to put...

Makes sense. I think the original issue here is (mostly) solved.

Related RFCs: * #4190 asks for `No goals` to point to errors elsewhere in the proof. #4190 is slightly incompatible with this feature request, because that RFC requests Lean to...

I expect that this will be a bit of whack-a-mole (see *Implementation speculation* in my first message). If it works in the 90% most common cases, that is already very...

This looks good. Here are a few more examples what you could encounter while typing a tactic line. I expect that the first 4 are solved by #7135? Maybe the...