Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-10-19 15:11
cacc297c
View on Github →
fix(tactic/norm_num): remove unnecessary argument to rat.cast_zero (
#4682
) See
Zulip thread
.
Estimated changes
Modified
src/tactic/norm_num.lean
modified
theorem
norm_num.adc_bit0_bit1
modified
theorem
norm_num.adc_bit1_bit0
modified
theorem
norm_num.adc_bit1_bit1
modified
theorem
norm_num.int_div
modified
theorem
norm_num.int_mod
modified
theorem
norm_num.le_bit0_bit0
modified
theorem
norm_num.le_bit1_bit1
modified
theorem
norm_num.lt_bit0_bit0
modified
theorem
norm_num.lt_bit1_bit1
modified
theorem
norm_num.rat_cast_bit0
modified
theorem
norm_num.rat_cast_bit1
modified
theorem
norm_num.sle_bit0_bit0
modified
theorem
norm_num.sle_bit0_bit1
modified
theorem
norm_num.sle_bit1_bit0
modified
theorem
norm_num.sle_bit1_bit1
modified
theorem
norm_num.sle_one_bit0
modified
theorem
norm_num.sle_one_bit1
Modified
test/norm_num.lean