RFC lean#4318 Better error reports for incomplete calc

Stream: lean4

[Yaël Dillies]

This RFC was accepted. Am I expected to open a PR implementing it? I still haven't managed to get the infoview working when editing the lean4 repo...

[Sebastian Ullrich]

No, there is no expectation of implementing it. It just means that any submitted PR would now be reviewed for acceptance, or else we will implement it ourselves if and when we get to it, according to the applied priority label.

[Kim Morrison]

@Sebastian Ullrich, could we update the description text for "RFC accepted" to explicitly say "We will review an associated PR."?