feat: non-opaque `UInt64.toUSize`

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.74k stars 427 forks source link

feat: non-opaque `UInt64.toUSize` #6202

Closed tydeu closed 14 hours ago

tydeu commented 1 day ago

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 commented 1 day ago

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 commented 1 day ago

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 commented 1 day ago

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 commented 14 hours ago

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.