Commit 2021-02-02 14:43 893ce8b6

View on Github →

feat(tactic/norm_fin): tactic for normalizing fin n expressions (#5820) This is based on #5791, with a new implementation using the normalize_fin function.

Estimated changes

Created src/tactic/norm_fin.lean

added theorem tactic.norm_fin.normalize_fin.add

added theorem tactic.norm_fin.normalize_fin.bit0

added theorem tactic.norm_fin.normalize_fin.bit1

added theorem tactic.norm_fin.normalize_fin.cast

added theorem tactic.norm_fin.normalize_fin.eq

added theorem tactic.norm_fin.normalize_fin.le

added theorem tactic.norm_fin.normalize_fin.lt

added theorem tactic.norm_fin.normalize_fin.mul

added theorem tactic.norm_fin.normalize_fin.one

added theorem tactic.norm_fin.normalize_fin.reduce

added theorem tactic.norm_fin.normalize_fin.zero

added def tactic.norm_fin.normalize_fin

added theorem tactic.norm_fin.normalize_fin_iff

added theorem tactic.norm_fin.normalize_fin_lt.add_nat

added theorem tactic.norm_fin.normalize_fin_lt.cast

added theorem tactic.norm_fin.normalize_fin_lt.cast_add

added theorem tactic.norm_fin.normalize_fin_lt.cast_le

added theorem tactic.norm_fin.normalize_fin_lt.cast_lt

added theorem tactic.norm_fin.normalize_fin_lt.cast_succ

added theorem tactic.norm_fin.normalize_fin_lt.coe

added theorem tactic.norm_fin.normalize_fin_lt.lt

added theorem tactic.norm_fin.normalize_fin_lt.mk

added theorem tactic.norm_fin.normalize_fin_lt.nat_add

added theorem tactic.norm_fin.normalize_fin_lt.of

added theorem tactic.norm_fin.normalize_fin_lt.reduce

added theorem tactic.norm_fin.normalize_fin_lt.succ

added theorem tactic.norm_fin.normalize_fin_lt.zero

added def tactic.norm_fin.normalize_fin_lt

Modified src/tactic/norm_num.lean

Created test/norm_fin.lean