mathlib
3e7a56ee - feat(tactic/norm_num): support for nat.cast + int constructors (#6235)

Commit
4 years ago
feat(tactic/norm_num): support for nat.cast + int constructors (#6235) This adds support for the functions `nat.cast`, `int.cast`, `rat.cast` as well as `int.to_nat`, `int.nat_abs` and the constructors of int `int.of_nat` and `int.neg_succ_of_nat`, at least in their simp-normal forms.
Author
Parents
Loading