feat: non-opaque UInt64.toUSize

[tydeu]

This PR makes USize.toUInt64 a regular non-opaque definition.

It also moves it to Init.Data.UInt.Basic, as it is not actually used in Init.Prelude anymore.

[tydeu]

It is not entirely clear to me whether these definitions belong in Init.Data.UInt.Basic or Init.Data.UInt.BasicAux, because I do not know what the meta code BasicAux refers to is. I placed them in Init.Data.UInt.Basic because that is where the corresponding UInt32.toUSize and USize.toUInt32 definitions are.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6202 has successfully built against this PR. (2024-11-24 20:03:54) View Log
• ✅ Mathlib branch lean-pr-testing-6202 has successfully built against this PR. (2024-11-24 22:33:10) View Log
• ✅ Mathlib branch lean-pr-testing-6202 has successfully built against this PR. (2024-11-24 23:50:30) View Log

[digama0]

It is not entirely clear to me whether these definitions belong in Init.Data.UInt.Basic or Init.Data.UInt.BasicAux, because I do not know what the meta code BasicAux refers to is. I placed them in Init.Data.UInt.Basic because that is where the corresponding UInt32.toUSize and USize.toUInt32 definitions are.

As far as I am aware, the only reason BasicAux exists is because of bootstrapping / import cycle issues. So if you got it to compile in Basic then I think that's fine. (If you would like to find out why this division exists, I encourage you to try merging the two files and see what goes wrong.)

[hargoniX]

As far as I am aware, the only reason BasicAux exists is because of bootstrapping / import cycle issues. So if you got it to compile in Basic then I think that's fine.

Correct. The import cycle here is due to the fact that some UIntX stuff is used in conjunction with Array and from there with Syntax. For example the definition of the existential binder requires some UIntX stuff to already exist.