Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-01 04:36 6eedc0e7

View on Github →

feat(tactic/norm_num): rewrite norm_num to use simp instead of reflection

Estimated changes

Modified tactic/interactive.lean

Modified tactic/norm_num.lean

deleted theorem norm_num.bit0_le_one

deleted theorem norm_num.bit0_le_zero

added theorem norm_num.bit0_zero

deleted theorem norm_num.bit1_le_bit0

deleted theorem norm_num.bit1_le_one

deleted theorem norm_num.bit1_le_zero

added theorem norm_num.bit1_zero

added theorem norm_num.lt_add_of_pos_helper

deleted theorem norm_num.one_le_bit0

deleted theorem norm_num.one_le_bit1

deleted theorem norm_num.one_le_one

deleted theorem norm_num.pow_bit0

modified theorem norm_num.pow_bit0_helper

deleted theorem norm_num.pow_bit1

modified theorem norm_num.pow_bit1_helper

deleted theorem norm_num.pow_eq_pow_nat

deleted theorem norm_num.pow_eq_pow_nat_helper

deleted theorem norm_num.pow_one

deleted theorem norm_num.pow_zero

deleted theorem norm_num.zero_le_bit0

deleted theorem norm_num.zero_le_bit1

deleted theorem norm_num.zero_le_one

deleted theorem norm_num.zero_le_zero

deleted def num.add1

deleted def num.add_n

deleted theorem num.bit0_le_bit0

deleted theorem num.denote_add1

deleted theorem num.denote_le_denote_of_num_le

deleted theorem num.denote_le_denote_of_pos_num_le

deleted theorem num.denote_le_denote_of_znum_le

deleted def num.num_le

deleted theorem num.one_le_denote

deleted def num.pos_le

deleted theorem num.zero_le_denote

deleted def num.znum_le

deleted inductive tactic.interactive.denotation

deleted def tactic.interactive.znum.to_neg

deleted def tactic.interactive.znum.to_pos

Modified tests/norm_num.lean