status of data.nat.bits

Stream: mathlib4

[Arien Malec]

I think the whole thing is a "don't port" right? Because of the status of bit0/bit1 and Nat.bit in Lean 4? I assume bitwise goes the same direction?

[Mario Carneiro]

No, bitwise ops are definitely desirable

[Mario Carneiro]

However, I think this is going to go the same way as data.rbtree: while important, it will be implemented entirely in core/std and the files here will only be alignments

[Arien Malec]

I wondered whether there was something in Lean 4 that was more direct...

[Shreyas Srinivas]

@Mario Carneiro are there lists of such files which should not be ported in the usual way? I tried to port data.nat.bits before coming across this issue on this thread.

[Kevin Buzzard]

I think it's one of those "hive mind" things. Did nobody put a comment about this in the wiki port-status file? I think that's the best approach to make these things known, at least right now.

[Arien Malec]

Good call -- I'll do that rn.

[Arien Malec]

already done...

[Kevin Buzzard]

Yeah after I posted I realised that it was silly just telling people to do something when I could just do it myself :-)

[Siddhartha Gadgil]

Thanks for doing this, especially as it shows up in Commelin's list: https://math.commelin.net/files/port_status.html which is very useful.