List.rdrop

Stream: mathlib4

[Scott Morrison]

@Yakov Pechersky, how would you feel about renaming your List.rdrop to List.dropRight, to match e.g. String.dropRight?

[Yakov Pechersky]

Sounds fine to me

[Scott Morrison]

(I was trying to work out how to phrase the question to indicate a hope that you might do it yourself. :-)

[Yury G. Kudryashov]

Adding this little detail after "yes" looks like cheating to me ;)

[Scott Morrison]

The "you" and "your" in the original message were intended to convey a sense of custodianship. :-)

[Yakov Pechersky]

I'll take on the custodian (janitor) role

[Damiano Testa]

Scott Morrison said:

(I was trying to work out how to phrase the question to indicate a hope that you might do it yourself. :-)

Very subtle

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib4/pull/8233