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 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