Archive and Counterexamples label

Stream: mathlib4

[Daniel Weber]

Should there be labels for PRs in Archive/Counterexamples, perhaps named t-archive and t-counterexamples?

[Bryan Gin-ge Chen]

Since the t-blah labels are mostly used by reviewers to find PRs and vice versa, I think it might be more useful to label those PRs with the labels that correspond most closely with their mathematical content.

[Jon Eugster]

That being said, if you personally would find it useful to have such a label (for whatever reason), one could definitely think about adding such labels. For example, I recently created an IMO label upon request by users contributing IMO problems.

[Damiano Testa]

Maybe, there could be extra allowed PR title beginnings, like "Archive: ...", as there are "feat:", "chore:",...

[Daniel Weber]

I think feat(Archive/...): is clear enough