Commit 2021-11-19 07:29 f7390292

View on Github →

feat(Data/UInt, Data/Fin/Basic) declarations (#90) Add new Fin instances, extend the UInt declarations to other UInt types using a macro. This incorporates @gebner's suggestions to add boolean methods for checking under/overflow, and adding separate instances of Fin size. I still can't figure out the elaboration issue mentioned here on zulip, so I can't use the macro on USize yet.

Estimated changes

deleted theorem Fin.add_assoc
deleted theorem Fin.add_comm
modified theorem Fin.add_def
deleted theorem Fin.add_left_neg
deleted theorem Fin.add_zero
deleted def Fin.gsmul
deleted theorem Fin.gsmul_neg'
deleted theorem Fin.gsmul_succ'
deleted theorem Fin.gsmul_zero'
added theorem Fin.mod_def
added theorem Fin.mod_eq_of_lt
added theorem Fin.mod_eq_val
added theorem Fin.mod_lt
modified theorem Fin.modn_def
deleted theorem Fin.mul_comm
modified theorem Fin.mul_def
deleted def Fin.nsmul
deleted theorem Fin.nsmul_succ'
deleted theorem Fin.nsmuls_eq
deleted theorem Fin.of_nat_zero
added theorem Fin.one_def:
deleted theorem Fin.positive_size
added theorem Fin.size_positive'
added theorem Fin.size_positive
modified theorem Fin.sub_def
deleted theorem Fin.sub_eq_add_neg
added theorem Fin.val_eq_of_lt
deleted theorem Fin.val_one
deleted theorem Fin.val_zero
deleted theorem Fin.zero_add
added theorem Fin.zero_def
deleted theorem Fin.zero_mul
added theorem zero_lt_of_lt
added theorem $typeName.add_def
added theorem $typeName.eq_of_val_eq
added theorem $typeName.mk_val_eq
added theorem $typeName.mod_def
added theorem $typeName.mul_def
added theorem $typeName.neg_def
added theorem $typeName.one_def
added theorem $typeName.sub_def
added theorem $typeName.val_eq_of_eq
added theorem $typeName.zero_def
deleted theorem Fin.val_eq_of_lt
added theorem UInt16.size_positive
added theorem UInt16.val_eq_of_lt
added theorem UInt32.size_positive
modified theorem UInt32.val_eq_of_lt
added theorem UInt64.size_positive
added theorem UInt64.val_eq_of_lt
added theorem UInt8.size_positive
added theorem UInt8.val_eq_of_lt
added theorem USize.size_positive
added theorem USize.val_eq_of_lt