align private decls

Stream: mathlib4

[Johan Commelin]

(how) should we #align private declarations?

[Ruben Van de Velde]

I've removed the #aligns - it's not like they can be used for anything

[Reid Barton]

Should we be silently discarding private? Does private exist in Lean 4?

[Shreyas Srinivas]

I used this chat as a reference to do just that https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/align.20private.20decls/near/317107099

[Shreyas Srinivas]

with a porting note

[Shreyas Srinivas]

Lean4 did not allow access to the private def name

[Shreyas Srinivas]

It suggested _private.....<def_name>, but that also gave an error.

[Shreyas Srinivas]

Reid Barton said:

Should we be silently discarding private? Does private exist in Lean 4?

It is possible that lean4 is complaining that I should not be able to access that def. If so, this suggests that lean 4 definitely recognizes private as a keyword that should restrict access

[Mario Carneiro]

yes private exists. Yes we should remove #align on private decls

[Reid Barton]

And should they stay private in mathlib 4?

[Mario Carneiro]

I think so?

[Mario Carneiro]

the effect is basically the same, so I don't see why not

[Mario Carneiro]

I mean private declarations are discouraged in mathlib to begin with, but I don't think that the move to lean 4 has anything to do with that

[Reid Barton]

Makes sense to me, I was just wondering because I came across a lemma that lost its private modifier in the port.

[Mario Carneiro]

hm, mathport didn't do that

[Eric Wieser]

Does mathport currently attempt to emit #aligns for private decls?

[Shreyas Srinivas]

It did for me.

[Ruben Van de Velde]

Yeah, it does

[Ruben Van de Velde]

Maybe that's simple enough to fix

[Mario Carneiro]

it does (PR's welcome)