I think it is better to keep the more restrictive grammar for a more uniform look, although it might be reasonable to parse the alternative if only to give a better error message. (Note that lean 3 allowed you to put |- anywhere and even repeat it, and although I don't know for sure I think the grammar simplification was deliberate.)

I agree; just a more informative error message would be fine.

We just discussed this. I think being more liberal (turnstile anywhere in the list) is desirable from a UX stand-point. I certainly have tried it, it failed, and I gave up (rather than figuring out that the turnstyle has to come last). I think we’d do our users a favor of being more liberal here. (Forcing the turnstyle last could be a style linter if people care.)

Hopefully allowing something like (term <|> turnstyle)* as the parser is fine.

Hopefully allowing something like (term <|> turnstyle)* as the parser is fine.

This was indeed the case. One thing I was wondering about: do we want to reimplement the Lean 3 behavior exactly and defer any stylistic preferences to linters down the line? Or are there any constraints we want to enforce or warn about within the elaborator itself?

As was mentioned above, under the Lean 3 approach, rw [foo] at ⊢ and rw [foo] at ⊢ h ⊢ are permissible. The latter is consistent with the current situation in Lean 4 for rewriting at hypotheses, which allows things like rw [foo] at h h h without any warnings. Aside from its stylistic suboptimality, I suppose there's a chance that this could be misinterpreted as repeatedly performing the given tactic at the hypothesis (edit: apparently this is tactic-dependent: rw will repeatedly rewrite, whereas simp generates new inaccessible local declarations)—though I don't think this has been reported as an actual source of confusion anywhere that I've seen.

I'd kick that can down the road. Nobody complained about at h h, and it seems even less likely that people will accidentally use the turnstile twice. So doesn't seem to matter either way.

That said, if it's simple to detect and complain about duplicates while you are touching the code anyways maybe do it, before people discover this “feature” and use it to do repeated rewrites :-)