Not sure if the tag v4.5.0 was appropriate. Please change if necessary. Also, please add a status tag (WIP, awaiting-review, awaiting-author) unless that doesn't make sense.

I guess the draft PR status duplicates the WIP label information?

Anyways, once we know when leanprover/lean4#3040 will land we'll know when to proceed here.

WIP

Thanks! It's really just to help managing the PR queue, even if the info is duplicated.

Have you considered ignoring draft PRs in the queue?

I do but it's not that common to use draft PRs on Std. Most people just keep those on their own forks. It only takes a second look for a draft but WIP just takes one look and it's at the same place as all the other useful info.

Got it, will try to remember to WIP my draft PRs!

I'm closing this, as it's already been merged to both nightly-testing and bump/v4.6.0.