leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.75k stars 427 forks source link

feat: `USize.reduceToNat` #6190

Closed tydeu closed 3 hours ago

tydeu commented 5 days ago

This PR adds the builtin simproc USize.reduceToNat which reduces the USize.toNat operation on literals less than UInt32.size (i.e., 4294967296).

leanprover-community-bot commented 5 days ago

Mathlib CI status (docs):