e17e0d36a7
This is very helpful when dealing with bitvectors, where a case analysis on the bitwidth leaves one with hypotheses of the form `x<2^(Nat.succ w)`. Design decisions I am unsure about: - Is creating a helper `succ?` the correct way to match on the exponent `e+1`? - I'm not certain why the prior call to `Int.ofNat_pow` also checked that the exponent was a ground natural. I removed this, since we now explicitly handle cases where the exponent is a term of the form `e+1`. --------- Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Joe Hendrix <joe@lean-fro.org> Co-authored-by: Alex Keizer <alex@keizer.dev> |
||
|---|---|---|
| .. | ||
| Basic.lean | ||
| Bitwise.lean | ||
| DivMod.lean | ||
| DivModLemmas.lean | ||
| Gcd.lean | ||
| Lemmas.lean | ||
| Order.lean | ||