Deprecated since 2022

Stream: mathlib4

[Yury G. Kudryashov]

I'm looking at the definitions and lemmas deprecated since 2022. In some cases, it's not clear what's the substitute. E.g., what about docs#castPosNum and nearby definitions?

[Yury G. Kudryashov]

According to #607, these defs are deprecated because they use bit0 and bit1. I'm going to unfold bit* in their definitions instead of deleting them.

[Michael Rothgang]

Thank you for looking into this. Just as a data point: I tried simply removing these declarations - this failed; they are used somewhere in mathlib.

[Jon Eugster]

I remember that during the port it was definitely a thing to blindly add deprecation attrs to anything using bit* without much thinking about whether the statement is used or not. So it may well be that your approach of avoiding to use bit* is completely correct and the deprecation attr may therefore be removed again?

[Johan Commelin]

That sounds very reasonable to me.

[Yury G. Kudryashov]

About Num: I started #13627 but marked it as help-wanted and please-adopt. The lazy way is to disable the linter in the Lemmas file again. The proper way is to drop all references to bit0 and bit1 in that file.

[Yury G. Kudryashov]

@Mario Carneiro What do you want to happen to docs#bit0 and docs#bit1 ? They are no longer used for numeric literals but they are used for docs#Num, authored by (according to the copyright header) Leo and you. I assume that if Leo cared about it, he would move it to core, so probably you're the person who cares most about this file and its dependencies.

[Mario Carneiro]

you should just be able to replace bit0 n and bit1 n with 2*n and 2*n+1 respectively. They are not used in any way in Num incompatibly with that

[Mario Carneiro]

although Num has constructors named bit0 and bit1 which should be left as is

[Yury G. Kudryashov]

What's the right binary recursion in Lean 4?

[Mario Carneiro]

the same one?

[Mario Carneiro]

IIRC Nat.binaryRecOn still exists

[Yury G. Kudryashov]

OK