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: add missing UInt bitwise toNat theorems #6187

Closed tydeu closed 2 days ago

tydeu commented 2 days ago

This PR adds toNat_ theorems for the or, xor, shiftLeft, and shiftRight operations of the UInt types. It also renames and_toNat to toNat_and to fit with the current naming convention.

tydeu commented 2 days ago

Closed in favor of #6188.