feat: add simps and `toNat` lemmas for `UIntX` types

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

242 stars 101 forks source link

Closed fgdorais closed 3 months ago

fgdorais commented 3 months ago

Reported by @eric-wieser on Zulip.

Some lemmas are about val instead of toNat so they may need update if core changes the implementation of UIntX types.

fgdorais commented 3 months ago

would be nice to have ofNat lemmas for UInt64.toUInt32 etc too, but that doesn't have to be in this PR.

These are not as trivial, so another PR is best to avoid overloading this one.