Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-10-24 22:57 2dd035a6

View on Github →

Merge remote-tracking branch 'cipher1024/master'

Estimated changes

Created meta/expr.lean

Created tactic/norm_num.lean

added theorem norm_num.bit0_le_one

added theorem norm_num.bit0_le_zero

added theorem norm_num.bit1_le_bit0

added theorem norm_num.bit1_le_one

added theorem norm_num.bit1_le_zero

added theorem norm_num.one_le_bit0

added theorem norm_num.one_le_bit1

added theorem norm_num.one_le_one

added theorem norm_num.pow_bit0

added theorem norm_num.pow_bit0_helper

added theorem norm_num.pow_bit1

added theorem norm_num.pow_bit1_helper

added theorem norm_num.pow_eq_pow_nat

added theorem norm_num.pow_eq_pow_nat_helper

added theorem norm_num.pow_one

added theorem norm_num.pow_zero

added theorem norm_num.zero_le_bit0

added theorem norm_num.zero_le_bit1

added theorem norm_num.zero_le_one

added theorem norm_num.zero_le_zero

added def num.add1

added def num.add_n

added theorem num.bit0_le_bit0

added theorem num.denote_add1

added theorem num.denote_le_denote_of_num_le

added theorem num.denote_le_denote_of_pos_num_le

added theorem num.denote_le_denote_of_znum_le

added def num.num_le

added theorem num.one_le_denote

added def num.pos_le

added theorem num.zero_le_denote

added def num.znum_le

added inductive tactic.interactive.denotation

added def tactic.interactive.znum.to_neg

added def tactic.interactive.znum.to_pos

Created tests/norm_num.lean