Mario Carneiro

If this is to be used for general message formatting, I strongly recommend `of_string : string -> message`, since not all message sources are structured and you need a fallback...

This looks like a bug in the if-then compilation strategy for matches. It is producing a term of the form `ite (n = 0) T E : P n`, but...

The mathlib port is going to want the same behavior as lean 3, which FTR is: ```lean example {n} (h : n = 0) : n = 0 := by...

Oh, that's an interesting idea. It will need tweaking to calibrate how annoying it is; users might not be in the mood to think about performance depending on what they...

Keep in mind that `return` in do-notation is an *early exit*, it is not `pure`. So it is reasonable to me that using `return`, especially in `if` conditions, will produce...

Ah, I misinterpreted your point. Ignore that first sentence.

> > But to really solve the TCO issue in general, including all the do sugar (the usual definition of "tail position" would not exclude these examples), what is needed...

> I would blame, more specifically, the imperative if . Sure. The do notation desugaring is a big and complicated thing in lean 4, and there are several possible ways...

Mathlib has a linter framework: https://leanprover-community.github.io/mathlib_docs/commands.html#linting%20commands . Some of this should probably be incorporated into the core lean 4 distribution, but the details have not been worked out. (My impression...

Let's close this issue now that the linter framework has been implemented, and reopen issues for specific linters.