refactor: Adjust to new termination_by syntax

[nomeata]

this makes the necessary changes to compile with the termination_by
syntax refactoring in leanprover/lean4#3040.

[fgdorais]

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.

[nomeata]

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.

[nomeata]

WIP

[fgdorais]

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

[nomeata]

Have you considered ignoring draft PRs in the queue?

[fgdorais]

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.

[nomeata]

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

[kim-em]

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