Indentation after classical

Stream: mathlib4

[Andrew Yang]

Should we indent after the tactic classical? To me, classical is just a abbreviation for have := Classical.propDecidable so there shouldn't be one, but it seems that it is indented at times? For example here. What is the concensus on this?

[Johan Commelin]

If you indent, then it limits the scope of that have.

[Johan Commelin]

So in certain proofs, it might even be necessary to indent.

[Kyle Miller]

There are quite a few times classical is indented that are purely a consequence of mathport using the tactic pretty printer. I think we've agreed that the style is not to indent (unless you want to limit the scope for some reason).

[Andrew Yang]

I see. Thanks for the replies!

[Damiano Testa]

By the way, I initially found space sensitivity a nuisance, until I internalised more the difference between a tactic and a tacticSeq.

[Mario Carneiro]

Kyle Miller said:

There are quite a few times classical is indented that are purely a consequence of mathport using the tactic pretty printer. I think we've agreed that the style is not to indent (unless you want to limit the scope for some reason).

classical contains a pretty printer annotation telling it to not indent, so this doesn't sound correct. (Indeed, we have the opposite problem: a classical which does not scope over the whole remainder of the block will be pretty printed incorrectly because it doesn't indent.)

[Kyle Miller]

That's because you fixed it in the meantime :smile: #4519